coe_le_coe — Mathlib

English

The pointwise order on simple functions agrees with the induced preorder: ⇑f ≤ ⇑g iff f ≤ g.

Русский

Пусть сравнение функций проводится по значениям на каждой точке; тогда сравнение лексикографическое по значениям функций эквивалентно порядку функций f ≤ g.

LaTeX

$$$\\bigl(\\forall a, f(a) \\le g(a)\\bigr) \\iff f \\le g.$$$

Lean4

@[norm_cast]
theorem coe_le_coe : ⇑f ≤ g ↔ f ≤ g :=
  .rfl

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