regularSpace_iInf — Mathlib

English

If each index i yields a regular space X_i, then the infimum across i is regular.

Русский

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

LaTeX

$$$\forall i, RegularSpace(X_i) \Rightarrow RegularSpace(iInf\ t)$$$

Lean4

theorem regularSpace_iInf {ι X} {t : ι → TopologicalSpace X} (h : ∀ i, @RegularSpace X (t i)) :
    @RegularSpace X (iInf t) :=
  regularSpace_sInf <| forall_mem_range.mpr h

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