instT5SpaceSubtype

Mathlib.Topology.Separation.Regular

URI: https://scilib.ai/kg/mathlib#instT5SpaceSubtype

English

If X is T5, then the subtype { x : X | p x } is T5.

Русский

Если X — T5, то подпространство { x ∈ X | p x } тоже T5.

LaTeX

$$$ [T5Space X] \\Rightarrow [T5Space (Subtype (fun x => p x))]$$$

Lean4

/-- A subspace of a T₅ space is a T₅ space. -/
instance [T5Space X] {p : X → Prop} : T5Space { x // p x } :=
  IsEmbedding.subtypeVal.t5Space

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

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

Разделы

Аффилиация

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