t25Space — Mathlib

English

If X ≃ₜ Y is a homeomorphism and Y is a T25-space, then X is a T25-space; conversely, T25 passes along the inverse homeomorphism.

Русский

Если существует гомеморфизм X ≃ₜ Y и Y является T25-пространством, то X тоже T25-пространство.

LaTeX

$$$[\text{Homeomorphism } h: X\cong Y] \; (T25 Space\; Y)\Rightarrow T25 Space\; X.$$$

Lean4

protected theorem t25Space [TopologicalSpace Y] [T25Space X] (h : X ≃ₜ Y) : T25Space Y :=
  h.symm.isEmbedding.t25Space

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