le_egauge_closedBall_one — Mathlib

English

The gauge on the unit closed ball bounds the norm function from above by 1: egauge 𝕜 (closedBall 0 1) x ≥ ||x||.

Русский

Шкала на единичном замкнутом сфере ограничивает норму сверху: ||x|| ≤ egauge 𝕜 (closedBall 0 1) x.

LaTeX

$$$\\forall x:\\; \\|x\\|_{e} \\le \\operatorname{egauge}_{\\mathbb{k}}(\\overline{B}(0,1),x).$$$

Lean4

theorem le_egauge_closedBall_one (x : E) : ‖x‖ₑ ≤ egauge 𝕜 (closedBall 0 1) x := by
  simpa using div_le_egauge_closedBall 𝕜 1 x

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