English
Let M be a preorder with a zero element. The pointwise embedding of finitely supported M-valued functions into all functions, Finsupp.toFun : (ι →₀ M) → ι → M, preserves order: if f ≤ g (coordinatewise), then Finsupp.toFun f ≤ Finsupp.toFun g.
Русский
Пусть M — порядковая структура с нулём. Прямая отправка из функций с конечной опорой в функции \(ι → M\), Finsupp.toFun : (ι →₀ M) → ι → M, сохраняет порядок: если f ≤ g (по координатам), то Finsupp.toFun f ≤ Finsupp.toFun g.
LaTeX
$$$\\forall f,g:\\; ι \\to₀ M,\\; f \\le g \\Rightarrow (Finsupp.toFun\\, f) \\le (Finsupp.toFun\\, g).$$$
Lean4
theorem coe_strictMono : Monotone (Finsupp.toFun : (ι →₀ M) → ι → M) := fun _ _ ↦ id
