regularSpace_sInf — Mathlib

English

If each in a family T consists of regular spaces, then the infimum topology is regular.

Русский

Если каждый элемент семейства T образует регулярное пространство, то инфимум топологий является регулярным.

LaTeX

$$$\forall t \in T, RegularSpace X \Rightarrow RegularSpace X (sInf T)$$$

Lean4

theorem regularSpace_sInf {X} {T : Set (TopologicalSpace X)} (h : ∀ t ∈ T, @RegularSpace X t) :
    @RegularSpace X (sInf T) := by
  let _ := sInf T
  have :
    ∀ a,
      (𝓝 a).HasBasis
        (fun If : Σ I : Set T, I → Set X => If.1.Finite ∧ ∀ i : If.1, If.2 i ∈ @nhds X i a ∧ @IsClosed X i (If.2 i))
        fun If => ⋂ i : If.1, If.snd i :=
    fun a ↦ by
    rw [nhds_sInf, ← iInf_subtype'']
    exact .iInf fun t : T => @closed_nhds_basis X t (h t t.2) a
  refine .of_hasBasis this fun a If hIf => isClosed_iInter fun i => ?_
  exact (hIf.2 i).2.mono (sInf_le (i : T).2)

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