English
The join of two complemented elements is realized by pairing their underlying joins with the join of their complement proofs: if a,b have proofs ha,hb, then ⟨a,ha⟩ ⊔ ⟨b,hb⟩ = ⟨a ⊔ b, ha.sup hb⟩.
Русский
Объединение двух дополненных реализуется как пара: основание ⟨a,ha⟩ и ⟨b,hb⟩ объединяются в ⟨a ⊔ b, ha.sup hb⟩.
LaTeX
$$$\forall a,b\in \mathrm{Complementeds}(\alpha)\ (ha,b h_b)\text{ with } ha,hb:\ IsComplemented(a), IsComplemented(b),\ (⟨a,ha⟩ \lor ⟨b,hb⟩) = ⟨a \lor b, ha.sup hb⟩$$$
Lean4
@[simp]
theorem mk_sup_mk {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
(⟨a, ha⟩ ⊔ ⟨b, hb⟩ : Complementeds α) = ⟨a ⊔ b, ha.sup hb⟩ :=
rfl
