div_le_egauge_ball — Mathlib

English

For r ≥ 0 and x ∈ E, the div-inequality holds: ||x||/r ≤ egauge 𝕜 (ball 0 r) x.

Русский

Для r≥0 и x верно: ||x||/r ≤ egauge 𝕜 (ball 0 r) x.

LaTeX

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

Lean4

theorem div_le_egauge_ball (r : ℝ≥0) (x : E) : ‖x‖ₑ / r ≤ egauge 𝕜 (ball 0 r) x :=
  (div_le_egauge_closedBall 𝕜 r x).trans <| egauge_anti _ ball_subset_closedBall _

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