instR0SpaceSubtype

Mathlib.Topology.Separation.Basic

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

English

The subtype of a space X by a predicate p inherits R0 from X.

Русский

Подпространство {x ∈ X | p(x)} наследует свойство R0 от X.

LaTeX

$$$R0Space(\\mathrm{Subtype}(p))$$$

Lean4

instance {p : X → Prop} : R0Space { x // p x } :=
  IsInducing.subtypeVal.r0Space

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

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

Разделы

Аффилиация

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