English
Let α be a semiring and (β_i) a family of α-modules with a compatible partial order and canonical ordered addition. If each SMulPosReflectLT α (β_i) holds, then SMulPosReflectLT α (Π₀ i, β_i) holds as well; i.e., finite-support functions inherit the SMulPosReflectLT property componentwise.
Русский
Пусть α — полугруппа, и для каждого i имеется семейство β_i модулей над α с совместимым частичным порядком и канонически упорядоченным сложением. Тогда, если для каждого i выполняется свойство SMulPosReflectLT α (β_i), то это свойство верно и для DFinsupp fun i => β_i, то есть для пространства функций с конечной поддержкой.
LaTeX
$$$\\bigl(\\forall i,\\ SMulPosReflectLT\\,\\alpha\\ (\\beta_i)\\bigr) \\Rightarrow SMulPosReflectLT\\,\\alpha\\ (\\Pi_0 i,\\ \\beta_i).$$$
Lean4
instance instSMulPosReflectLT [∀ i, SMulPosReflectLT α (β i)] : SMulPosReflectLT α (Π₀ i, β i) :=
SMulPosReflectLT.lift _ coe_le_coe coe_smul coe_zero
