absorbent_ball_zero — Mathlib

English

Balls around the origin are absorbent: for any r > 0, the ball centered at 0 with radius r is absorbent.

Русский

Шары вокруг нуля поглощательны: при любом r > 0 шар с центром в 0 и радиусом r поглощает пространство.

LaTeX

$$$0 < r \Rightarrow \text{Absorbent } 𝕜 (\mathrm{Metric.ball}(0,E,r)).$$$

Lean4

/-- Balls at the origin are absorbent. -/
theorem absorbent_ball_zero (hr : 0 < r) : Absorbent 𝕜 (Metric.ball (0 : E) r) :=
  by
  rw [← ball_normSeminorm 𝕜]
  exact (normSeminorm _ _).absorbent_ball_zero hr

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