monotone_addNSMul — Mathlib

English

If t lies in [addNSMul h δ n, addNSMul h δ (n+1)], then |t − addNSMul h δ n| ≤ δ, assuming δ ≥ 0.

Русский

Если t лежит между соседними членами addNSMul, то расстояние от t до addNSMul h δ n не превосходит δ, при δ ≥ 0.

LaTeX

$$δ ≥ 0 ⇒ {t ∈ Icc a b} → (t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n+1)) → |t - addNSMul h δ n| ≤ δ)$$

Lean4

theorem monotone_addNSMul (hδ : 0 ≤ δ) : Monotone (addNSMul h δ) := fun _ _ hnm ↦
  monotone_projIcc h <| (add_le_add_iff_left _).mpr (nsmul_le_nsmul_left hδ hnm)

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