instT25Space

Mathlib.Topology.Separation.Regular

URI: https://scilib.ai/kg/mathlib#Subtype.instT25Space

English

If X is a T25-space, then the subtype {x ∈ X | p x} with any predicate p is also a T25-space.

Русский

Если X является T25-пространством, то подпространство {x ∈ X | p x} тоже является T25-пространством.

LaTeX

$$$[T25Space X] \Rightarrow [T25Space \{x\,|\, p x\}].$$$

Lean4

instance instT25Space [T25Space X] {p : X → Prop} : T25Space { x // p x } :=
  IsEmbedding.subtypeVal.t25Space

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

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

Разделы

Аффилиация

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