instComplementedLattice — Mathlib

English

The complemented elements carry a complemented lattice structure, with a complement operation defined by swapping the two components: comp(⟨a,b,h⟩) = ⟨b,a,h.symm⟩, and IsCompl is transported accordingly.

Русский

Дополненные элементы образуют дополненную решётку; дополнение элемента достигается обменом координат: comp(⟨a,b,h⟩) = ⟨b,a,h.symm⟩, и IsCompl переносится соответствующе.

LaTeX

$$$\text{ComplementedLattice}(\mathrm{Complementeds}(\alpha))\;:\; x=(a,b,h)\mapsto \langle b,a,h^{\mathrm{symm}}\rangle,\; \text{IsCompl}(x) = \text{IsCompl}(a,b).$$$

Lean4

instance : ComplementedLattice (Complementeds α) :=
  ⟨fun ⟨a, b, h⟩ => ⟨⟨b, a, h.symm⟩, isCompl_coe.1 h⟩⟩

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