Necessity.lean

1import BFPP.ClopenPairs2import BFPP.SignRealization34/-! # Necessity of extremal disconnectedness for the ball fixed point property -/56namespace BFPP78set_option autoImplicit false910variable {K : Type*} [TopologicalSpace K] [CompactSpace K] [T2Space K]1112theorem not_hasBFPP_of_FSpace_not_ED (hF : IsFSpace K) (hED : ¬ ExtremallyDisconnected K) :13    ¬ HasBFPP C(K, ℝ) := by14  by_cases hsep : TotallySeparatedSpace K15  · letI : TotallySeparatedSpace K := hsep16    exact not_hasBFPP_of_zeroDimensional_not_ED hED17  · exact not_hasBFPP_of_not_totallySeparated hF hsep1819/-- The necessity direction of the paper's characterization, including both topological cases. -/20theorem extremallyDisconnected_of_hasBFPP (h : HasBFPP C(K, ℝ)) : ExtremallyDisconnected K := by21  by_contra hED22  exact not_hasBFPP_of_FSpace_not_ED (isFSpace_of_hasBFPP h) hED h2324theorem exists_nonexpansive_fixedPointFree_of_not_ED (hED : ¬ ExtremallyDisconnected K) :25    ∃ T : UnitBall C(K, ℝ) → UnitBall C(K, ℝ), LipschitzWith 1 T ∧ ∀ f, T f ≠ f := by26  classical27  by_contra hn28  apply hED29  apply extremallyDisconnected_of_hasBFPP30  intro T hT31  by_contra hfix32  apply hn33  exact ⟨T, hT, fun f hf => hfix ⟨f, hf⟩⟩3435end BFPP

SHA-256