str_eq_of_le_nhds — Mathlib

English

If the ultrafilter map sends F to x and F.lim ≤ nhds x, then the structure map equals x.

Русский

Если отображение ультрафильтра отправляет F в x и F.lim ≤ nhds x, то структура равна x.

LaTeX

$$$X.str F = x \\Rightarrow \\; \\uparrow F \\leq \\mathcal{N}x$$$

Lean4

theorem str_eq_of_le_nhds {X : Compactum} (F : Ultrafilter X) (x : X) : ↑F ≤ 𝓝 x → X.str F = x := by
  -- Notation to be used in this proof.

  let fsu := Finset (Set (Ultrafilter X))
  let ssu := Set (Set (Ultrafilter X))
  let ι : fsu → ssu := fun x ↦ ↑x
  let T0 : ssu := {S | ∃ A ∈ F, S = basic A}
  let AA := X.str ⁻¹' { x }
  let T1 := insert AA T0
  let T2 := finiteInterClosure T1
  intro cond
  have claim1 : ∀ A : Set X, IsClosed A → A ∈ F → x ∈ A :=
    by
    intro A hA h
    by_contra H
    rw [le_nhds_iff] at cond
    specialize cond Aᶜ H hA.isOpen_compl
    rw [Ultrafilter.mem_coe, Ultrafilter.compl_mem_iff_notMem] at cond
    contradiction
      -- If A ∈ F, then x ∈ cl A.

  have claim2 : ∀ A : Set X, A ∈ F → x ∈ cl A := by
    intro A hA
    exact
      claim1 (cl A) (isClosed_cl A)
        (mem_of_superset hA (subset_cl A))
          -- T0 is closed under intersections.

  have claim3 : ∀ (S1) (_ : S1 ∈ T0) (S2) (_ : S2 ∈ T0), S1 ∩ S2 ∈ T0 :=
    by
    rintro S1 ⟨S1, hS1, rfl⟩ S2 ⟨S2, hS2, rfl⟩
    exact
      ⟨S1 ∩ S2, inter_mem hS1 hS2, by simp [basic_inter]⟩
        -- For every S ∈ T0, the intersection AA ∩ S is nonempty.

  have claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty := by
    rintro S ⟨S, hS, rfl⟩
    rcases claim2 _ hS with ⟨G, hG, hG2⟩
    exact
      ⟨G, hG2, hG⟩
        -- Every element of T0 is nonempty.

  have claim5 : ∀ S ∈ T0, Set.Nonempty S := by
    rintro S ⟨S, hS, rfl⟩
    exact
      ⟨F, hS⟩
        -- Every element of T2 is nonempty.

  have claim6 : ∀ S ∈ T2, Set.Nonempty S :=
    by
    suffices ∀ S ∈ T2, S ∈ T0 ∨ ∃ Q ∈ T0, S = AA ∩ Q by
      intro S hS
      rcases this _ hS with h | h
      · exact claim5 S h
      · rcases h with ⟨Q, hQ, rfl⟩
        exact claim4 Q hQ
    intro S hS
    apply finiteInterClosure_insert
    · constructor
      · use Set.univ
        refine ⟨Filter.univ_sets _, ?_⟩
        ext
        refine ⟨?_, by tauto⟩
        · intro
          apply Filter.univ_sets
      · exact claim3
    · exact hS
  suffices ∀ F : fsu, ↑F ⊆ T1 → (⋂₀ ι F).Nonempty
    by
    obtain ⟨G, h1⟩ := Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty _ this
    have c1 : X.join G = F := Ultrafilter.coe_le_coe.1 fun P hP => h1 (Or.inr ⟨P, hP, rfl⟩)
    have c2 : G.map X.str = X.incl x :=
      by
      refine Ultrafilter.coe_le_coe.1 fun P hP => ?_
      apply mem_of_superset (h1 (Or.inl rfl))
      rintro x ⟨rfl⟩
      exact hP
    simp [← c1, c2]
      -- Finish...

  intro T hT
  refine claim6 _ (finiteInter_mem (.finiteInterClosure_finiteInter _) _ ?_)
  intro t ht
  exact finiteInterClosure.basic (@hT t ht)

Похожие утверждения