compl_bihimp_compl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem compl_bihimp_compl : aᶜ ⇔ bᶜ = a ⇔ b :=
  @compl_symmDiff_compl αᵒᵈ _ _ _

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