closedBall_eq_sphere_of_nonpos — Mathlib

English

If ε ≤ 0, then the closed ball equals the sphere with the same center and radius.

Русский

Если ε ≤ 0, то замкнутый шар равен сфере с тем же центром и радиусом.

LaTeX

$$ε ≤ 0 ⇒ \\overline{B}(x, ε) = \\mathrm{sphere}(x, ε)$$

Lean4

/-- Closed balls and spheres coincide when the radius is non-positive -/
theorem closedBall_eq_sphere_of_nonpos (hε : ε ≤ 0) : closedBall x ε = sphere x ε :=
  Set.ext fun _ => (hε.trans dist_nonneg).ge_iff_eq'

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