sup_eq_top_of_ne — Mathlib

English

Let a and b be coatoms in a semilattice with a top element, and suppose a ≠ b. Then a ⊔ b equals the top element.

Русский

Пусть a и b — коатомы в полупорядоченном множестве с верхним элементом, и a ≠ b. Тогда a ⊔ b = ⊤.

LaTeX

$$$ IsCoatom\ a \to IsCoatom\ b \to a \neq b \to a \lor b = \top $$$

Lean4

theorem sup_eq_top_of_ne (ha : IsCoatom a) (hb : IsCoatom b) (hab : a ≠ b) : a ⊔ b = ⊤ :=
  codisjoint_iff.1 <| ha.codisjoint_of_ne hb hab

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