of_le — Mathlib

English

In a lattice with bounds, if x and y are disjoint (x ∧ y = ⊥) and cover the universe (x ∨ y = ⊤), then x and y are complements.

Русский

В решётке с границами, если x и y не имеют общего элемента и их объединение охватывает всё множество, то x и y являются комплементарными.

LaTeX

$$$$ (x \wedge y = \bot) \rightarrow (y \leq \top) \\ (x \vee y = \top) \rightarrow IsCompl(x,y). $$$$

Lean4

theorem of_le (h₁ : x ⊓ y ≤ ⊥) (h₂ : ⊤ ≤ x ⊔ y) : IsCompl x y :=
  ⟨disjoint_iff_inf_le.mpr h₁, codisjoint_iff_le_sup.mpr h₂⟩

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