English
The ball at 0 absorbs a smaller ball at the origin: there exists r>0 so that the ball at radius r absorbs p.ball 0 r2.
Русский
Шар в начале всасывает меньший шар в начале: существует r>0, такой, что шар радиуса r всасывает шар радиуса r2.
LaTeX
$$Absorbent 𝕜 (ball p (0: E) r) for some r>0$$
Lean4
/-- Seminorm-balls at the origin are absorbent. -/
protected theorem absorbent_ball_zero (hr : 0 < r) : Absorbent 𝕜 (ball p (0 : E) r) :=
absorbent_iff_forall_absorbs_singleton.2 fun _ =>
(p.ball_zero_absorbs_ball_zero hr).mono_right <| singleton_subset_iff.2 <| p.mem_ball_zero.2 <| lt_add_one _