update_strictMono — Mathlib

English

For a fixed i, the map update f i is strictly monotone: if x < y then (update f i) x < (update f i) y.

Русский

Для фиксированного i отображение update f i строго монотонно: если x < y, то (update f i) x < (update f i) y.

LaTeX

$$$\forall x\,y:\, x < y \rightarrow (\mathrm{update}\ f\ i)\ x < (\mathrm{update}\ f\ i)\ y$$$

Lean4

theorem update_strictMono : StrictMono (update f i) := fun _ _ => update_lt_update_iff.2

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