closure_ball — Mathlib

English

The closed ball equals the image of the corresponding preimage under the Euclidean identification.

Русский

Замкнутая шаровая оболочка равна образу соответствующего предобразования под евклидовым отображением.

LaTeX

$$closedBall x r = toEuclidean.symm '' Metric.closedBall (toEuclidean x) r$$

Lean4

nonrec theorem closure_ball (x : E) {r : ℝ} (h : r ≠ 0) : closure (ball x r) = closedBall x r := by
  rw [ball_eq_preimage, ← toEuclidean.preimage_closure, closure_ball (toEuclidean x) h, closedBall_eq_preimage]

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