SignExtension.lean

1import BFPP.Cozero2import Mathlib.Topology.UrysohnsLemma3import Mathlib.Topology.Sets.Closeds45/-! # Sign extension and the fresh-value argument -/67namespace BFPP89set_option autoImplicit false1011open Set TopologicalSpace1213universe u14variable {K : Type u} [TopologicalSpace K] [CompactSpace K]1516theorem exists_sign_extension [NormalSpace K] (U V : Set K)17    (hUV : Disjoint (closure U) (closure V)) :18    ∃ h : UnitBall C(K, ℝ), (∀ t ∈ closure U, h.val t = 1) ∧19      (∀ t ∈ closure V, h.val t = -1) := by20  obtain ⟨f, hfV, hfU, hf⟩ := exists_continuous_zero_one_of_isClosed21    isClosed_closure isClosed_closure hUV.symm22  let h : C(K, ℝ) := ⟨fun t => 2 * f t - 1, by fun_prop⟩23  have hnorm : ‖h‖ ≤ 1 := by24    apply (ContinuousMap.norm_le _ (by norm_num)).mpr25    intro t26    change |2 * f t - 1| ≤ 127    have ht := hf t28    exact abs_le.mpr ⟨by linarith [ht.1], by linarith [ht.2]⟩29  refine ⟨⟨h, hnorm⟩, ?_, ?_⟩30  · intro t ht31    change 2 * f t - 1 = 132    have he : f t = 1 := hfU ht33    rw [he]34    norm_num35  · intro t ht36    change 2 * f t - 1 = -137    have he : f t = 0 := hfV ht38    rw [he]39    norm_num4041theorem IsFSpace.disjoint_sign_closures (hK : IsFSpace K) (h : C(K, ℝ)) :42    Disjoint (closure {t | 0 < h t}) (closure {t | h t < 0}) := by43  let p : C(K, ℝ) := ⟨fun t => max (h t) 0, h.continuous.max continuous_const⟩44  let n : C(K, ℝ) := ⟨fun t => max (-h t) 0, h.continuous.neg.max continuous_const⟩45  have hp : {t | p t ≠ 0} = {t | 0 < h t} := by46    ext t47    change max (h t) 0 ≠ 0 ↔ 0 < h t48    simp only [ne_eq, max_eq_right_iff, not_le]49  have hn : {t | n t ≠ 0} = {t | h t < 0} := by50    ext t51    change max (-h t) 0 ≠ 0 ↔ h t < 052    simp only [ne_eq, max_eq_right_iff, not_le, neg_pos]53  have hd : Disjoint {t | p t ≠ 0} {t | n t ≠ 0} := by54    rw [hp, hn]55    apply Set.disjoint_left.mpr56    intro t ht ht'57    change 0 < h t at ht58    change h t < 0 at ht'59    linarith60  have hd' := hK p n hd61  simpa only [hp, hn] using hd'6263/-- The ordered pair of points cannot be separated by a clopen set. -/64def ClopenInseparable (p q : K) : Prop := ∀ s : Clopens K, p ∈ s → q ∈ s6566theorem exists_intermediate_value_of_clopenInseparable (p q : K)67    (hpq : ClopenInseparable p q) (h : UnitBall C(K, ℝ))68    (hp : h.val p = 1) (hq : h.val q = -1) :69    ∃ t, 0 < |h.val t| ∧ |h.val t| < 1 := by70  by_contra hnone71  have heq : ∀ t, 0 < h.val t → h.val t = 1 := by72    intro t ht73    have hl : 1 ≤ |h.val t| := by74      by_contra hl75      exact hnone ⟨t, by simpa only [abs_of_pos ht] using ht, lt_of_not_ge hl⟩76    rw [abs_of_pos ht] at hl77    exact le_antisymm (continuousBall_bounds h t).2 hl78  have hset : {t | 0 < h.val t} = {t | h.val t = 1} := by79    ext t80    constructor81    · exact heq t82    · intro ht83      change 0 < h.val t84      rw [ht]85      norm_num86  have hclosed : IsClosed {t | 0 < h.val t} := by87    rw [hset]88    exact isClosed_eq h.val.continuous continuous_const89  have hopen : IsOpen {t | 0 < h.val t} := isOpen_lt continuous_const h.val.continuous90  let s : Clopens K := ⟨{t | 0 < h.val t}, hclosed, hopen⟩91  have hps : p ∈ s := by change 0 < h.val p; rw [hp]; norm_num92  have hqs := hpq s hps93  change 0 < h.val q at hqs94  rw [hq] at hqs95  norm_num at hqs9697end BFPP

SHA-256