English
Let α_i be a family of preordered sets and consider the finite-support dependent functions f,g: i ↦ α_i. The natural map sending f to the function i ↦ f(i) embeds the DFinsupp into the product ∏_i α_i and preserves the order, i.e., the strict order on DFinsupp coincides with the strict product order of their pointwise values: (coe f) < (coe g) iff f < g.
Русский
Пусть α_i — семейство множеств с заданным порядком, а f,g: i ↦ α_i — функции с конечной опорой. Естественное отображение f ↦ (f(i)) является вложением DFinsupp в произведение ∏_i α_i и сохраняет порядок, причём строгий порядок DFinsupp совпадает с точечным порядком в произведении: (coe f) < (coe g) тогда и только тогда, когда f < g.
LaTeX
$$$$\big( (\forall i, f(i) \le g(i)) \wedge \exists i, f(i) \neq g(i) \big) \iff f < g.$$$$
Lean4
@[simp, norm_cast]
theorem coe_lt_coe : ⇑f < g ↔ f < g :=
Iff.rfl
