instCompletelyRegularSpaceForall — Mathlib

English

If X is T35 then T3 and so on (CR regularity transfers).

Русский

Из свойств T35 следует регулярность, и CR переносится на родовые структуры.

LaTeX

$$$[T35Space X] \\Rightarrow [T3Space X]$$$

Lean4

instance {ι : Type*} {X : ι → Type*} [t : Π (i : ι), TopologicalSpace (X i)]
    [ht : Π (i : ι), CompletelyRegularSpace (X i)] : CompletelyRegularSpace (Π i, X i) :=
  completelyRegularSpace_iInf (fun i => completelyRegularSpace_induced (ht i) _)

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