instRegularSpaceSubtype

Mathlib.Topology.Separation.Regular

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

English

For any predicate p on X, the subtype {x ∈ X : p(x)} inherits a regular space structure.

Русский

Подпространство {x ∈ X : p(x)} наследует регулярное пространство.

LaTeX

$$$\text{instance } RegularSpace(\text{Subtype } p)$$$

Lean4

instance {p : X → Prop} : RegularSpace (Subtype p) :=
  IsEmbedding.subtypeVal.isInducing.regularSpace

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

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

Разделы

Аффилиация

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