instR1SpaceSubtype

Mathlib.Topology.Separation.Basic

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

English

An instance giving R1Space on a Subtype p from R1Space X via induced topology.

Русский

Экземпляр, задающий R1-пространство на подпорождении через индуцированную топологию.

LaTeX

$$R1Space(Subtype p)$$

Lean4

instance (p : X → Prop) : R1Space (Subtype p) :=
  .induced _

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

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

Разделы

Аффилиация

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