lean_workbook_plus_24004
ProvedShow that is a retract of
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_24004 : ∃ f : ℝ → ℝ, ∀ x, f x ∈ Set.Icc 0 1 ∧ f 0 = 0 ∧ f 1 = 1 := by sorry
Source
Show that is a retract of
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_24004 : ∃ f : ℝ → ℝ, ∀ x, f x ∈ Set.Icc 0 1 ∧ f 0 = 0 ∧ f 1 = 1 := by sorry