instIsEquiv_compl

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#Ne.instIsEquiv_compl

English

The complement of inequality is an equivalence relation; in particular, equality is an equivalence.

Русский

Дополнение к неравенству образует эквивалентность; в частности, равенство — эквиваленция.

LaTeX

$$$ \text{IsEquiv}(\alpha, (\neq)^{c}) $$$

Lean4

instance instIsEquiv_compl : IsEquiv α (· ≠ ·)ᶜ :=
  by
  convert eq_isEquiv α
  simp [compl]

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

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

Разделы

Аффилиация

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