English
If the ball B(0,r) is contained in a set s, then for every x we have r · gauge(s, x) ≤ ||x||; in particular this holds with the usual convention for r ≤ 0 by the monotonicity of gauge.
Русский
Если шар B(0,r) содержится в множестве s, то для каждого x выполняется r · gauge(s, x) ≤ ||x||; эта неравенство сохраняется и при r ≤ 0 за счёт монотонности gauge.
LaTeX
$$$$ B(0,r) \subseteq s \implies r \cdot \mathrm{gauge}(s)\,x \le \|x\| \quad \text{для всех } x, $$$$
Lean4
theorem mul_gauge_le_norm (hs : Metric.ball (0 : E) r ⊆ s) : r * gauge s x ≤ ‖x‖ :=
by
obtain hr | hr := le_or_gt r 0
· exact (mul_nonpos_of_nonpos_of_nonneg hr <| gauge_nonneg _).trans (norm_nonneg _)
rw [mul_comm, ← le_div_iff₀ hr, ← gauge_ball hr.le]
exact gauge_mono (absorbent_ball_zero hr) hs x
