bihimp_eq_bot — Mathlib

English

An element pair a,b in a Boolean algebra satisfies a ⇔ b = ⊥ if and only if a and b are complements.

Русский

Элементы a,b булевой алгебры удовлетворяют a ⇔ b = ⊥ тогда и только тогда, когда a и b являются дополнениями друг к другу.

LaTeX

$$$ a \Leftrightarrow b = \bot \\iff IsCompl(a,b) $$$

Lean4

@[simp]
theorem bihimp_eq_bot : a ⇔ b = ⊥ ↔ IsCompl a b := by
  rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff, codisjoint_iff]

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