closedBall_eq_biInter_ball — Mathlib

English

The closedBall can be expressed as the intersection over all radii greater than r of the corresponding balls: closedBall p x r = ⋂_{ρ>r} ball p x ρ.

Русский

Замкнутый шар есть пересечение шаров с радиусами > r: closedBall p x r = ⋂_{ρ>r} ball p x ρ.

LaTeX

$$$\\mathrm{closedBall}_p(x,r) = \\bigcap_{\\rho>r} \\mathrm{ball}_p(x,\\rho)$$$

Lean4

theorem closedBall_eq_biInter_ball (x r) : closedBall p x r = ⋂ ρ > r, ball p x ρ := by ext y;
  simp_rw [mem_closedBall, mem_iInter₂, mem_ball, ← forall_gt_iff_le]

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