English
The infimum of two sublattices is their intersection, i.e., L ∧ M corresponds to L ∩ M.
Русский
Нижняя граница двух подрешеток есть их пересечение.
LaTeX
$$$ Min (Sublattice\\,\\alpha)\\,\\text{min}(L,M) = \\{\\text{carrier}=L \\cap M,\\; \\text{supClosed'}=L.supClosed\\cap M.supClosed,\\; \\text{infClosed'}=L.infClosed\\cap M.infClosed\\}$$$
Lean4
/-- The inf of two sublattices is their intersection. -/
instance instInf : Min (Sublattice α) where
min L
M :=
{ carrier := L ∩ M
supClosed' := L.supClosed.inter M.supClosed
infClosed' := L.infClosed.inter M.infClosed }