Characterization.lean

1import BFPP.Necessity2import BFPP.EDSupremum3import BFPP.BallOrderGeometry4import BFPP.LatticeFixedPoint56/-! # Characterization of the ball fixed point property for C(K, ℝ) -/78namespace BFPP910set_option autoImplicit false1112variable {K : Type*} [TopologicalSpace K] [CompactSpace K]1314theorem hasBFPP_of_extremallyDisconnected [ExtremallyDisconnected K] : HasBFPP C(K, ℝ) := by15  letI : CompleteLattice (UnitBall C(K, ℝ)) := edBallCompleteLattice16  intro T hT17  apply fixedPoint_of_interval_balls ?_ continuousBall_midpoint_radius T hT18  intro x r hr19  exact ⟨ballLower x r hr, ballUpper x r hr, continuousBall_closedBall_eq_Icc x r hr⟩2021/-- Main characterization, with both implications proved from mathlib. -/22theorem hasBFPP_iff_extremallyDisconnected [T2Space K] :23    HasBFPP C(K, ℝ) ↔ ExtremallyDisconnected K := by24  refine ⟨extremallyDisconnected_of_hasBFPP, ?_⟩25  intro h26  letI : ExtremallyDisconnected K := h27  exact hasBFPP_of_extremallyDisconnected2829theorem not_ED_iff_exists_fixedPointFree [T2Space K] :30    ¬ ExtremallyDisconnected K ↔31      ∃ T : UnitBall C(K, ℝ) → UnitBall C(K, ℝ), LipschitzWith 1 T ∧ ∀ f, T f ≠ f := by32  refine ⟨exists_nonexpansive_fixedPointFree_of_not_ED, ?_⟩33  rintro ⟨T, hT, hfree⟩ hED34  exact not_hasBFPP_of_fixedPointFree T hT hfree (hasBFPP_iff_extremallyDisconnected.mpr hED)3536end BFPP

SHA-256