sup_eq_top_iff — Mathlib

English

If a is a coatom, then for any b, a ⊔ b = ⊤ if and only if b is not below a (i.e., ¬(b ≤ a)).

Русский

Пусть a — коатом. Тогда для любого b верно: a ⊔ b = ⊤ тогда и только тогда, когда b не ниже a (¬(b ≤ a)).

LaTeX

$$$ IsCoatom\ a \to (a \lor b = \top \iff \neg (b \le a)) $$$

Lean4

@[deprecated not_le_iff_codisjoint (since := "2025-07-11")]
theorem sup_eq_top_iff (ha : IsCoatom a) : a ⊔ b = ⊤ ↔ ¬b ≤ a :=
  ha.dual.inf_eq_bot_iff

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