English
There is a complemented lattice structure on Complementeds α given by the swap construction; this provides the complement operation and ensures IsCompl matches under the swap.
Русский
Существует структура дополненной решётки на Complementeds α, заданная обменом координат; это обеспечивает операцию дополнения и совместимо с IsCompl.
LaTeX
$$$\text{ComplementedLattice}(\mathrm{Complementeds}(\alpha))\;:\; \langle a,b,h\rangle^c = \langle b,a,h^{\mathrm{symm}}\rangle,\; \text{IsCompl}(\langle a,b,h\rangle) = \text{IsCompl}(a,b).$$$
Lean4
/-- The function mapping `i` to `f i \ (⨆ j < i, f j)`. When `ι` is a partial order, this is the
unique function `g` having the same `partialSups` as `f` and such that `g i` and `g j` are
disjoint whenever `i < j`. -/
def disjointed (f : ι → α) (i : ι) : α :=
f i \ (Iio i).sup f
