ne_iff

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Codisjoint.ne_iff

English

For a codisjoint pair, a ≠ b is equivalent to a ≠ ⊤ or b ≠ ⊤.

Русский

Для кодиссоединённой пары не равенство a и b эквивалентно a ≠ ⊤ или b ≠ ⊤.

LaTeX

$$$\operatorname{Codisjoint}(a,b) \to (a \neq b) \leftrightarrow (a \neq \top) \lor (b \neq \top)$$$

Lean4

theorem ne_iff (hab : Codisjoint a b) : a ≠ b ↔ a ≠ ⊤ ∨ b ≠ ⊤ :=
  hab.eq_iff.not.trans not_and_or

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

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

Разделы

Аффилиация

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