instT1SpaceForall — Mathlib

English

If each X_i is a T1-space, then the product space ∀ i, X_i is a T1-space.

Русский

Если для каждого i пространство X_i является T1-пространством, то произведение ∀ i, X_i — T1-пространство.

LaTeX

$$$ \forall ι {X : ι \to Type*}, [\forall i, TopologicalSpace (X i)] [\forall i, T1Space (X i)] \\Rightarrow T1Space (\forall i, X i)$.$$

Lean4

instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T1Space (X i)] : T1Space (∀ i, X i) :=
  ⟨fun f => univ_pi_singleton f ▸ isClosed_set_pi fun _ _ => isClosed_singleton⟩

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