div_le_egauge_closedBall — Mathlib

English

For any r ≥ 0, the norm of x divided by r is bounded above by egauge 𝕜 of the closed ball with radius r around 0.

Русский

Для r ≥ 0 выполнено: ||x||/r ≤ egauge 𝕜 (closedBall 0 r) x.

LaTeX

$$$\\forall r\\in \\mathbb{R}_{\\ge 0},\\; \\frac{\\|x\\|}{r} \\le \\operatorname{egauge}_{\\mathbb{k}}(\\overline{B}(0,r),x).$$$

Lean4

theorem div_le_egauge_closedBall (r : ℝ≥0) (x : E) : ‖x‖ₑ / r ≤ egauge 𝕜 (closedBall 0 r) x :=
  by
  rw [le_egauge_iff]
  rintro c ⟨y, hy, rfl⟩
  rw [mem_closedBall_zero_iff, ← coe_nnnorm, NNReal.coe_le_coe] at hy
  rw [enorm_smul]
  apply ENNReal.div_le_of_le_mul
  gcongr
  rwa [enorm_le_coe]

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