English
The complemented elements of a distributive lattice form a lattice under the join operation, obtained coordinatewise from the ambient lattice: if a = ⟨A, hA⟩ and b = ⟨B, hB⟩ are complemented elements, then a ⊔ b is defined to be ⟨A ⊔ B, hA.sup hB⟩, i.e., the underlying element is A ⊔ B and the complemented-structure proof is the join of the two proofs.
Русский
Дополненные элементы распределённой решётки образуют решётку, при операции объединения, которая берётся по координатам из окружающей множества: если a = ⟨A, hA⟩ и b = ⟨B, hB⟩ являются дополненными, то a ⊔ b определяется как ⟨A ⊔ B, hA.sup hB⟩, то есть основанный элемент равен A ⊔ B, а доказательство сопряжённости – это сумма доказательств.
LaTeX
$$$\forall a,b\in \mathrm{Complementeds}(\alpha),\ a\lor b = \langle a.\mathrm{val} \lor b.\mathrm{val},\ a.\mathrm{proof}.sup b.\mathrm{proof} \rangle$$$
Lean4
instance : Max (Complementeds α) :=
⟨fun a b => ⟨a ⊔ b, a.2.sup b.2⟩⟩
