English
The complemented elements of a distributive lattice form a lattice under the meet 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.inf hB⟩.
Русский
Дополненные элементы распределённой решётки образуют решётку, при операции пересечения, которая берётся по координатам из окружающей множности: если a = ⟨A, hA⟩ и b = ⟨B, hB⟩, то a ⊓ b определяется как ⟨A ⊓ B, hA.inf hB⟩.
LaTeX
$$$\forall a,b\in \mathrm{Complementeds}(\alpha),\ a\land b = \langle a.\mathrm{val} \land b.\mathrm{val},\ a.\mathrm{proof}.inf b.\mathrm{proof} \rangle$$$
Lean4
instance : Min (Complementeds α) :=
⟨fun a b => ⟨a ⊓ b, a.2.inf b.2⟩⟩
