instT3SpaceForall — Mathlib

English

If each X_i is T3Space, then the space of all functions i ↦ X_i (the product) is T3Space.

Русский

Если каждый X_i — T3-пространство, то пространство всех функций i ↦ X_i (произведение) является T3-пространством.

LaTeX

$$$[\forall i, T3Space (X_i)] \Rightarrow T3Space (\forall i, X_i).$$$

Lean4

instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T3Space (X i)] : T3Space (∀ i, X i) :=
  ⟨⟩

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