exists_minimal_nonempty_closed_subset

English

In a compact space X, for any nonempty closed S ⊆ X there exists a nonempty closed V ⊆ S that is minimal (with respect to inclusion) among nonempty closed subsets of S; equivalently, any nonempty closed V' ⊆ V must satisfy V' = V.

Русский

В компактном пространстве X существует для любой непустой замкнутой подмножества S ⊆ X минимальное непустое замкнутое подмножество V ⊆ S, такое что любые непустые замкнутые подмножества V внутри V совпадают с V.

LaTeX

$$$ [\operatorname{CompactSpace}(X)] \land \operatorname{IsClosed}(S) \land S \neq \emptyset \Rightarrow \exists V \subseteq S,\ V \neq \emptyset,\ \operatorname{IsClosed}(V) \land \forall V'\subseteq V,\ V' \neq \emptyset \land \operatorname{IsClosed}(V') \Rightarrow V' = V. $$$

Lean4

theorem exists_minimal_nonempty_closed_subset [CompactSpace X] {S : Set X} (hS : IsClosed S) (hne : S.Nonempty) :
    ∃ V : Set X, V ⊆ S ∧ V.Nonempty ∧ IsClosed V ∧ ∀ V' : Set X, V' ⊆ V → V'.Nonempty → IsClosed V' → V' = V :=
  by
  let opens := {U : Set X | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
  obtain ⟨U, h⟩ :=
    zorn_subset opens fun c hc hz => by
      by_cases hcne : c.Nonempty
      · obtain ⟨U₀, hU₀⟩ := hcne
        haveI : Nonempty { U // U ∈ c } := ⟨⟨U₀, hU₀⟩⟩
        obtain ⟨U₀compl, -, -⟩ := hc hU₀
        use ⋃₀ c
        refine ⟨⟨?_, ?_, ?_⟩, fun U hU _ hx => ⟨U, hU, hx⟩⟩
        · exact fun _ hx => ⟨U₀, hU₀, U₀compl hx⟩
        · exact isOpen_sUnion fun _ h => (hc h).2.1
        · convert_to (⋂ U : { U // U ∈ c }, U.1ᶜ).Nonempty
          · ext
            simp only [not_exists, not_and, Set.mem_iInter, Subtype.forall, mem_compl_iff, mem_sUnion]
          apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
          · rintro ⟨U, hU⟩ ⟨U', hU'⟩
            obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'
            exact ⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩
          · exact fun U => (hc U.2).2.2
          · exact fun U => (hc U.2).2.1.isClosed_compl.isCompact
          · exact fun U => (hc U.2).2.1.isClosed_compl
      · use Sᶜ
        refine ⟨⟨Set.Subset.refl _, isOpen_compl_iff.mpr hS, ?_⟩, fun U Uc => (hcne ⟨U, Uc⟩).elim⟩
        rw [compl_compl]
        exact hne
  obtain ⟨Uc, Uo, Ucne⟩ := h.prop
  refine ⟨Uᶜ, Set.compl_subset_comm.mp Uc, Ucne, Uo.isClosed_compl, ?_⟩
  intro V' V'sub V'ne V'cls
  have : V'ᶜ = U :=
    by
    refine h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)
    · exact Set.Subset.trans Uc (Set.subset_compl_comm.mp V'sub)
    · simp only [compl_compl, V'ne]
  rw [← this, compl_compl]

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