codisjoint_of_ne

Mathlib.Order.Atoms

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

← MathLib Explorer

English

If a and b are coatoms and a ≠ b, then Codisjoint(a,b).

Русский

Если a и b — коатомы и a ≠ b, то Codisjoint(a,b).

LaTeX

$$$ \\mathrm{IsCoatom}(a) \\rightarrow \\mathrm{IsCoatom}(b) \\rightarrow a \\neq b \\rightarrow \\mathrm{Codisjoint}(a,b).$$$

Lean4

theorem codisjoint_of_ne (ha : IsCoatom a) (hb : IsCoatom b) (hab : a ≠ b) : Codisjoint a b := by
  simp [← ha.not_le_iff_codisjoint, hb.le_iff, hab, ha.ne_top]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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