compl — Mathlib

English

In a Boolean algebra, the complementation map is strictly order-reversing: if a < b then not b < not a.

Русский

В буловой алгебре операция дополнения строго обращает порядок: если a < b, то не b < не a.

LaTeX

$$$\forall a,b\in \alpha:\ a

Lean4

/-- Taking complements as an order isomorphism to the order dual. -/ @[simps!] def compl : α ≃o αᵒᵈ where toFun := OrderDual.toDual ∘ HasCompl.compl invFun := HasCompl.compl ∘ OrderDual.ofDual left_inv := compl_compl right_inv := compl_compl (α := αᵒᵈ) map_rel_iff' := compl_le_compl_iff_le

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