closedBall_eq_image — Mathlib

English

The closed ball is equal to the image of a closed ball under the corresponding Euclidean identification.

Русский

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

LaTeX

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

Lean4

theorem closedBall_eq_image (x : E) (r : ℝ) :
    closedBall x r = toEuclidean.symm '' Metric.closedBall (toEuclidean x) r := by
  rw [toEuclidean.image_symm_eq_preimage, closedBall_eq_preimage]

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