coe_lt_coe — Mathlib

English

The pointwise order on functions agrees with the coerced Finsupp order: the function-level comparison ⇑f < g is equivalent to the Finsupp comparison f < g.

Русский

Пусть f и g — конечносоединённые функции; сравнение на уровне функций эквивалентно сравнению в самом Finsupp.

LaTeX

$$$(\uparrow f) < g \iff f < g.$$$

Lean4

@[simp, norm_cast]
theorem coe_lt_coe : ⇑f < g ↔ f < g :=
  .rfl

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