map_natCast_strictMono — Mathlib

English

The function ENat.map Nat.cast is strictly monotone on ENat; i.e., x < y implies ENat.map Nat.cast(x) < ENat.map Nat.cast(y).

Русский

Функция ENat.map Nat.cast строго монотонна: если x < y, то ENat.map Nat.cast(x) < ENat.map Nat.cast(y).

LaTeX

$$$$ \\text{StrictMono}(\\mathrm{ENat.map}(\\mathrm{Nat.cast})) $$$$

Lean4

theorem map_natCast_strictMono : StrictMono (map (Nat.cast : ℕ → α)) :=
  strictMono_map_iff.2 Nat.strictMono_cast

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