coe_mono — Mathlib

English

The coercion-to-function map Finsupp.toFun is monotone: if f ≤ g in Finsupp, then the corresponding functions satisfy f ≤ g pointwise.

Русский

Приведение к функции Finsupp.toFun монотонно: если f ≤ g в Finsupp, то функции f и g удовлетворяют f ≤ g по каждой координате.

LaTeX

$$$\text{Monotone}(\text{Finsupp.toFun}):\; f \le g \Rightarrow (f \mapsto f) \le (g \mapsto g).$$$

Lean4

theorem coe_mono : Monotone (Finsupp.toFun : (ι →₀ M) → ι → M) := fun _ _ ↦ id

Похожие утверждения