norm_midpoint_lt_iff — Mathlib

English

If ‖x‖ = ‖y‖, then the midpoint satisfies ‖(x+y)/2‖ < ‖x‖ if and only if x ≠ y.

Русский

Если ‖x‖ = ‖y‖, то середина отрезка имеет норму строго меньше ‖x‖ тогда, когда x ≠ y.

LaTeX

$$$\|x\| = \|y\| \Rightarrow \Big( \|\tfrac12(x+y)\| < \|x\| \iff x \neq y \Big).$$$

Lean4

theorem norm_midpoint_lt_iff (h : ‖x‖ = ‖y‖) : ‖(1 / 2 : ℝ) • (x + y)‖ < ‖x‖ ↔ x ≠ y := by
  rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ← div_eq_inv_mul,
    div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h, not_sameRay_iff_norm_add_lt, h]

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