dist_smul_add_one_sub_smul_le — Mathlib

English

For r in [0,1], the distance dist(r x + (1−r) y, x) is at most dist(y,x).

Русский

Для r в [0,1] расстояние dist(r x + (1−r) y, x) не превосходит dist(y,x).

LaTeX

$$$\\forall r \\in [0,1],\\; \\operatorname{dist}(r x + (1-r) y, x) \\le \\operatorname{dist}(y,x)$$$

Lean4

theorem dist_smul_add_one_sub_smul_le {r : ℝ} {x y : E} (h : r ∈ Icc 0 1) : dist (r • x + (1 - r) • y) x ≤ dist y x :=
  calc
    dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖ := by
      simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add, sub_right_comm]
    _ = (1 - r) * dist y x := by rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm']
    _ ≤ (1 - 0) * dist y x := by gcongr; exact h.1
    _ = dist y x := by rw [sub_zero, one_mul]

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