eq

Mathlib.Topology.Separation.Basic

URI: https://scilib.ai/kg/mathlib#Specializes.eq

English

In a T1 space, equality of points can be derived from specialization; otherwise, specialization is defined by equality.

Русский

В T1-пространстве специализация эквивалентна равенству точек.

LaTeX

$$eq in Specializes context.$$

Lean4

theorem eq [T1Space X] {x y : X} (h : x ⤳ y) : x = y :=
  t1Space_iff_specializes_imp_eq.1 ‹_› h

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

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

Разделы

Аффилиация

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