absorbent_ball — Mathlib

English

If a ball around x with radius r contains points close to the origin in a suitable way, it is absorbent.

Русский

Если шар вокруг точки x радиуса r содержит окрестности начала координат, он поглощателен.

LaTeX

$$$\forall x\in E,\ r>0:\; \text{Absorbent } 𝕜 (\mathrm{Metric.ball}(x,r)).$$$

Lean4

/-- Balls containing the origin are absorbent. -/
theorem absorbent_ball (hx : ‖x‖ < r) : Absorbent 𝕜 (Metric.ball x r) :=
  by
  rw [← ball_normSeminorm 𝕜]
  exact (normSeminorm _ _).absorbent_ball hx

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