specializes_eq_eq

Mathlib.Topology.Separation.Basic

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

English

The specialization relation equals equality as a function from pairs to propositions in a T1 space.

Русский

Отношение специализации равно отношению равенства как функция от пар точек.

LaTeX

$$$(\\cdot \\; ⤳ \\; \\cdot) = @Eq X$ in T1Space.$$

Lean4

@[simp]
theorem specializes_eq_eq [T1Space X] : (· ⤳ ·) = @Eq X :=
  funext₂ fun _ _ => propext specializes_iff_eq

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

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

Разделы

Аффилиация

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