specializes_of_eq

Mathlib.Topology.Inseparable

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

English

If x equals y, then x specializes to y.

Русский

Если x равно y, то x специализируется на y.

LaTeX

$$$$\forall X\ [\text{TopologicalSpace } X],\ \forall x,y:X,\ x=y \Rightarrow x \rightsquigarrow y.$$$$

Lean4

theorem specializes_of_eq (e : x = y) : x ⤳ y :=
  e ▸ specializes_refl x

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

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

Разделы

Аффилиация

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