CountablePairs.lean

1import BFPP.Cozero2import BFPP.Families3import Mathlib.Data.Countable.Defs45/-! # An inseparable pair on an F-space cannot have two countable channels -/67namespace BFPP89set_option autoImplicit false10open Set1112universe u v w13variable {K : Type u} [TopologicalSpace K] [CompactSpace K]1415theorem countable_union_cozero_indexed {ι : Type v} [Countable ι] (f : ι → C(K, ℝ)) :16    ∃ g : C(K, ℝ), {t | g t ≠ 0} = ⋃ i, {t | f i t ≠ 0} := by17  classical18  letI := Encodable.ofCountable ι19  let h : ℕ → C(K, ℝ) := fun n => (Encodable.decode (α := ι) n).elim 0 f20  obtain ⟨g, hg⟩ := countable_union_cozero h21  refine ⟨g, hg.trans ?_⟩22  ext t23  simp only [mem_iUnion, Set.mem_ofPred_eq]24  constructor25  · rintro ⟨n, hn⟩26    cases he : Encodable.decode (α := ι) n with27    | none => simp [h, he] at hn28    | some i => exact ⟨i, by simpa only [h, he, Option.elim_some] using hn⟩29  · rintro ⟨i, hi⟩30    exact ⟨Encodable.encode i, by simpa [h] using hi⟩3132theorem InseparablePair.false_of_countable_channels33    {ι : Type v} {κ : Type w} [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ]34    [Countable ι] [Countable κ] (F : InseparablePair K ι κ) (hK : IsFSpace K) : False := by35  obtain ⟨f, hf⟩ := countable_union_cozero_indexed F.positive.functions36  obtain ⟨g, hg⟩ := countable_union_cozero_indexed F.negative.functions37  have hdis : Disjoint {t | f t ≠ 0} {t | g t ≠ 0} := by38    rw [hf, hg]39    apply Set.disjoint_left.mpr40    intro t ht ht'41    obtain ⟨i, hi⟩ := mem_iUnion.mp ht42    obtain ⟨j, hj⟩ := mem_iUnion.mp ht'43    exact (mul_ne_zero hi hj) (F.orthogonal i j t)44  have hdis' := hK f g hdis45  rw [hf, hg] at hdis'46  have hp : (⋃ i, F.positive.levels i) ⊆ ⋃ i, {t | F.positive.functions i t ≠ 0} := by47    intro t ht48    obtain ⟨i, hi⟩ := mem_iUnion.mp ht49    refine mem_iUnion.mpr ⟨i, ?_⟩50    change F.positive.functions i t = 1 at hi51    change F.positive.functions i t ≠ 052    rw [hi]53    norm_num54  have hn : (⋃ j, F.negative.levels j) ⊆ ⋃ j, {t | F.negative.functions j t ≠ 0} := by55    intro t ht56    obtain ⟨j, hj⟩ := mem_iUnion.mp ht57    refine mem_iUnion.mpr ⟨j, ?_⟩58    change F.negative.functions j t = 1 at hj59    change F.negative.functions j t ≠ 060    rw [hj]61    norm_num62  exact (Set.not_disjoint_iff.mpr F.inseparable) (hdis'.mono (closure_mono hp) (closure_mono hn))6364end BFPP

SHA-256