norm_sub_le_of_mem_segment — Mathlib

English

If y lies in the segment between x and z in a normed space, then the distance from x to y is at most the distance from x to z.

Русский

Если y лежит в отрезке между x и z в нормированном пространстве, то расстояние от x до y не превосходит расстояния от x до z.

LaTeX

$$$\\forall x,y,z\\in E,\\; y \\in \\operatorname{segment}_{\\mathbb{R}} x z \\Rightarrow \\|y-x\\| \\le \\|z-x\\|$$$

Lean4

theorem norm_sub_le_of_mem_segment {x y z : E} (hy : y ∈ segment ℝ x z) : ‖y - x‖ ≤ ‖z - x‖ :=
  by
  rw [segment_eq_image'] at hy
  simp only [mem_image, mem_Icc] at hy
  obtain ⟨u, ⟨hu_nonneg, hu_le_one⟩, rfl⟩ := hy
  simp only [add_sub_cancel_left, norm_smul, Real.norm_eq_abs]
  rw [abs_of_nonneg hu_nonneg]
  conv_rhs => rw [← one_mul (‖z - x‖)]
  gcongr

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