biInter_gt_closedBall — Mathlib

English

For any x in a pseudometric space, the intersection over all radii r' > r of closed balls equals the closed ball of radius r.

Русский

Пересечение всех замкнутых шаров радиусов r′ > r равно замкнутому шару радиуса r около точки x.

LaTeX

$$$\bigcap_{r'>r} \mathrm{closedBall}(x,r') = \mathrm{closedBall}(x,r)$$$

Lean4

theorem biInter_gt_closedBall (x : α) (r : ℝ) : ⋂ r' > r, closedBall x r' = closedBall x r :=
  by
  ext
  simp [forall_gt_imp_ge_iff_le_of_dense]

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