norm_le_of_mem_closedBall' — Mathlib

English

If b ∈ closedBall a r then ∥b∥ ≤ ∥a∥ + r.

Русский

Если b принадлежит замкнутому шару вокруг a радиуса r, то ∥b∥ ≤ ∥a∥ + r.

LaTeX

$$$$ b \in \overline{\mathrm{Ball}}(a, r) \Rightarrow \|b\| \le \|a\| + r. $$$$

Lean4

@[to_additive norm_le_of_mem_closedBall]
theorem norm_le_of_mem_closedBall' (h : b ∈ closedBall a r) : ‖b‖ ≤ ‖a‖ + r :=
  (norm_le_norm_add_norm_div' _ _).trans <| add_le_add_left (by rwa [← dist_eq_norm_div]) _

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