t25Space — Mathlib

English

If f: X→Y is an embedding and Y is a T25-space, then X is a T25-space.

Русский

Если отображение f: X→Y вложение и Y является T25-пространством, то X тоже T25-пространство.

LaTeX

$$$\text{If } f: X\to Y\text{ is an embedding and } Y\text{ is T25},\text{ then } X\text{ is T25}.$$$

Lean4

theorem t25Space [TopologicalSpace Y] [T25Space Y] {f : X → Y} (hf : IsEmbedding f) : T25Space X :=
  .of_injective_continuous hf.injective hf.continuous

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