update_mono — Mathlib

English

For a fixed i, the update operation update f i : ι → π i is monotone in its input, i.e., if x ≤ y then (update f i) x ≤ (update f i) y.

Русский

Для фиксированного индекса i операция обновления update f i : ι → π i монотонна по входу: если x ≤ y, то (update f i) x ≤ (update f i) y.

LaTeX

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

Lean4

theorem update_mono : Monotone (update f i) := fun _ _ => update_le_update_iff'.2

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