t2Space — Mathlib

English

If each fiber Y(a) is a Hausdorff space, then the space of all sections (Pi-type) ∀a, Y(a) is Hausdorff.

Русский

Если для каждого a пространство Y(a) Хаусдорфово, то пространство всех функций a ↦ Y(a) (произведение) Хаусдорфово.

LaTeX

$$$ \\left( \\forall a, TopologicalSpace(Y(a)) \\right) \\land \\left( \\forall a, T2Space(Y(a)) \\right) \\Rightarrow T2Space\\left( \\prod_{a} Y(a) \\right)$$$

Lean4

instance t2Space {Y : X → Type v} [∀ a, TopologicalSpace (Y a)] [∀ a, T2Space (Y a)] : T2Space (∀ a, Y a) :=
  inferInstance

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