canLiftSet

Mathlib.Topology.Sets.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.OpenNhdsOf.canLiftSet

English

The auxiliary toOpens function is injective on OpenNhdsOf x.

Русский

Вспомогательная функция toOpens инъективна на OpenNhdsOf x.

LaTeX

$$$\operatorname{toOpens}\; : OpenNhdsOf x \to Opens(\alpha)$ инъективна$$

Lean4

instance canLiftSet : CanLift (Set α) (OpenNhdsOf x) (↑) fun s => IsOpen s ∧ x ∈ s :=
  ⟨fun s hs => ⟨⟨⟨s, hs.1⟩, hs.2⟩, rfl⟩⟩

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

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

Разделы

Аффилиация

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