English
If each α_i is a lattice, then the family Π₀ i, α_i of dependent finite-support functions forms a lattice with coordinatewise infimum and supremum.
Русский
Если каждая α_i образует решетку, то множество Π₀ i, α_i нормализуется в решетку, где на координатах inf и sup вычисляются по координатам.
LaTeX
$$$$ \text{If } \forall i, \mathcal{L}(\alpha_i) \text{ then } \Pi_0 i, \alpha_i \text{ is a lattice with } (f \inf g)(i) = f(i) \inf g(i),\; (f \sup g)(i) = f(i) \sup g(i). $$$$
Lean4
instance lattice : Lattice (Π₀ i, α i) :=
{ (inferInstance : SemilatticeInf (DFinsupp α)), (inferInstance : SemilatticeSup (DFinsupp α)) with }
