English
If M is a lattice with zero, then the collection of finitely supported M-valued functions ι →₀ M forms a lattice under the pointwise infimum and supremum.
Русский
Пусть M — решётка с нулём. Тогда множество функций с конечной опорой из ι в M образует решётку под точечно заданными операциями наименьшего и наибольшего.
LaTeX
$$$\\text{Lattice}(\\,\\iota \\to M\\,)$ with $$(f \\inf g)(i)=f(i) \\inf g(i),\\quad (f \\sup g)(i)=f(i) \\sup g(i).$$$$
Lean4
instance lattice : Lattice (ι →₀ M) where
__ := Finsupp.semilatticeInf
__ := Finsupp.semilatticeSup