absorbent_ball_zero — Mathlib

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 _

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