instT2Space — Mathlib

English

If β is a T2 space, then α →ᵤ β is a T2 space (the topology is Hausdorff).

Русский

Если β — пространство Т2, то α →ᵤ β — гамма, топология едина — Хаусдорфово.

LaTeX

$$$$ \text{If } β \text{ is } T_2, \ (α \to^{u} β) \text{ is } T_2. $$$$

Lean4

/-- The topology of uniform convergence is T₂. -/
instance [T2Space β] : T2Space (α →ᵤ β) :=
  .of_injective_continuous toFun.injective UniformFun.uniformContinuous_toFun.continuous

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