English
There is a bottom element in Lex(Π_i α_i) given by the zero function, which is ≤ every element.
Русский
В Lex(Π_i α_i) имеется нижний элемент, задаваемый нулевой функцией, который лежит не ниже любого элемента.
LaTeX
$$$$ \\text{bot} = 0 \\quad\\text{and}\\quad 0 \\le f \\text{ for all } f \\in \\mathrm{Lex}(\\\\Pi_i α_i) $$$$
Lean4
/-- Dependent functions with finite support inherit a module structure from such a structure on
each coordinate. -/
instance module [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] : Module γ (Π₀ i, β i) :=
{
inferInstanceAs
(DistribMulAction γ
(Π₀ i,
β i)) with
zero_smul := fun c => ext fun i => by simp only [smul_apply, zero_smul, zero_apply]
add_smul := fun c x y => ext fun i => by simp only [add_apply, smul_apply, add_smul] }
