English
Let α be a lattice. The infimum of any family S of Sublattice α is the intersection of their carriers; in particular, the carrier of sInf S is ⋂ L∈S (L as a set).
Русский
Пусть α — решётка. Непрерывное пересечение множества подрешёток α имеет каркас равной пересечению их носителей; в частности, множество носителей sInf S равно ⋂ L∈S (L как множество).
LaTeX
$$$(sInf\,S : \{\alpha\}) = \bigcap_{L \in S} (L : \mathrm{Set} \alpha)$$$
Lean4
/-- The inf of sublattices is their intersection. -/
instance instInfSet : InfSet (Sublattice α) where
sInf
S :=
{ carrier := ⨅ L ∈ S, L
supClosed' :=
supClosed_sInter <| forall_mem_range.2 fun L ↦ supClosed_sInter <| forall_mem_range.2 fun _ ↦ L.supClosed
infClosed' :=
infClosed_sInter <| forall_mem_range.2 fun L ↦ infClosed_sInter <| forall_mem_range.2 fun _ ↦ L.infClosed }
