closedBall_eq_bInter_ball — Mathlib

English

The closed ball with center x and radius ε equals the intersection of all open balls with center x and radius δ for δ > ε.

Русский

Замкнутый шар B̄(x, ε) равен пересечению всех открытых шаров B(x, δ) при δ > ε.

LaTeX

$$$ \overline{B}(x, \varepsilon) = \bigcap_{\delta>\varepsilon} B(x, \delta) $$$

Lean4

theorem closedBall_eq_bInter_ball : closedBall x ε = ⋂ δ > ε, ball x δ := by ext y;
  rw [mem_closedBall, ← forall_gt_iff_le, mem_iInter₂]; rfl

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