not_le_iff_disjoint

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#IsAtom.not_le_iff_disjoint

English

For an atom a, not_disjoint a b is equivalent to a ≤ b.

Русский

Для атома a неразделимое с b эквивалентно a ≤ b.

LaTeX

$$$ \\mathrm{IsAtom}(a) \\rightarrow \\big(\\lnot \\mathrm{Disjoint}(a,b) \\leftrightarrow a \\le b\\big).$$$

Lean4

theorem not_le_iff_disjoint (ha : IsAtom a) : ¬a ≤ b ↔ Disjoint a b :=
  ha.not_disjoint_iff_le.not_right.symm

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

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

Разделы

Аффилиация

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