norm_lt_of_mem_ball'

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#norm_lt_of_mem_ball'

← MathLib Explorer

English

If b ∈ ball a r, then ∥b∥ < ∥a∥ + r.

Русский

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

LaTeX

$$$$ b \in \mathrm{ball}(a, r) \Rightarrow \|b\| < \|a\| + r. $$$$

Lean4

@[to_additive norm_lt_of_mem_ball]
theorem norm_lt_of_mem_ball' (h : b ∈ ball a r) : ‖b‖ < ‖a‖ + r :=
  (norm_le_norm_add_norm_div' _ _).trans_lt <| add_lt_add_left (by rwa [← dist_eq_norm_div]) _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru