lean_workbook_plus_19946
ProvedFind the function that satisfies the given conditions: is continuous, , , and for all and , where represents the -th iterate of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19946 (x : ℝ) (n : ℕ) (f : ℝ → ℝ) (hf: f x = 0 ∧ f 1 = 1 ∧ ∀ x ∈ Set.Icc (0:ℝ) 1, (f^[n] x = x)) : ∃ f : ℝ → ℝ, f x = 0 ∧ f 1 = 1 ∧ ∀ x ∈ Set.Icc (0:ℝ) 1, (f^[n] x = x) := by sorry
Source