not_le_iff_codisjoint

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#IsCoatom.not_le_iff_codisjoint

English

Not b ≤ a is equivalent to Codisjoint(a,b) when a is a coatom.

Русский

Не (b ≤ a) эквивалентно Codisjoint(a,b), если a — коатом.

LaTeX

$$$ \\mathrm{IsCoatom}(a) \\rightarrow \\lnot (b \\le a) \\iff \\mathrm{Codisjoint}(a,b).$$$

Lean4

theorem not_le_iff_codisjoint (ha : IsCoatom a) : ¬b ≤ a ↔ Codisjoint a b :=
  ha.not_codisjoint_iff_le.not_right.symm

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

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

Разделы

Аффилиация

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