not_codisjoint_iff_le

Mathlib.Order.Atoms

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

← MathLib Explorer

English

If a is a coatom, not codisjoint with b is equivalent to b ≤ a.

Русский

Если a — коатом, то не_codisjoint(a,b) равно b ≤ a.

LaTeX

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

Lean4

theorem not_codisjoint_iff_le (ha : IsCoatom a) : ¬Codisjoint a b ↔ b ≤ a := by rw [codisjoint_iff, ← sup_eq_left];
  exact ha.ne_top_iff_eq le_sup_left

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

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

Разделы

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

Аффилиация

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