t1Space

Mathlib.Topology.Separation.Basic

URI: https://scilib.ai/kg/mathlib#Homeomorph.t1Space

English

If X and Y are homeomorphic and Y is a T1-space, then X is a T1-space.

Русский

Если X и Y гомеоморфны и Y — T1-пространство, то X тоже является T1-пространством.

LaTeX

$$$ \forall X,Y, h: X \cong_t Y, [TopologicalSpace Y], [T1Space Y] \Rightarrow T1Space X$.$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru