of_isTopologicalBasis — Mathlib

English

Any Noetherian space is quasi-separated.

Русский

Любое пространство Нетерена является квазиразделимым.

LaTeX

$$[NoetherianSpace α] ⇒ QuasiSeparatedSpace α$$

Lean4

theorem of_isTopologicalBasis {ι : Type*} {b : ι → Set α} (basis : IsTopologicalBasis (range b))
    (isCompact_inter : ∀ i j, IsCompact (b i ∩ b j)) : QuasiSeparatedSpace α where
  inter_isCompact U V hUopen hUcomp hVopen
    hVcomp :=
    by
    have aux :=
      isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis b basis fun i ↦ by simpa using isCompact_inter i i
    obtain ⟨s, hs, rfl⟩ := (aux _).1 ⟨hUcomp, hUopen⟩
    obtain ⟨t, ht, rfl⟩ := (aux _).1 ⟨hVcomp, hVopen⟩
    rw [iUnion₂_inter_iUnion₂]
    exact hs.isCompact_biUnion fun i hi ↦ ht.isCompact_biUnion fun j hj ↦ isCompact_inter ..

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