lean_workbook_plus_27916
ProvedBecause is strictly increasing and , then and . If or , then or . If and , because , then and . For the continuous in function there is , such that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27916 (f g : ℝ → ℝ) (h₁ : Continuous g) (h₂ : 0 ≤ g ∧ g ≤ 1) (h₃ : ∀ x y, 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 → x ≤ y → f x ≤ f y) (h₄ : ∀ x y, 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 → x < y → f x < f y) (h₅ : g 0 = 0 ∨ g 1 = 1) (h₆ : f 0 = 0 ∧ f 1 = 1) : ∃ x, g x = x := by sorry
Source