closedBall_eq_preimage — Mathlib

English

The ball around x with radius r equals the preimage of the metric ball around toEuclidean x with radius r under the Euclidean identification.

Русский

Окрестность x радиуса r равна предобразованию метрического шара вокруг toEuclidean x радиуса r по Евклидову соответствию.

LaTeX

$$ball x r = toEuclidean^{-1}'(Metric.ball (toEuclidean x) r)$$

Lean4

theorem closedBall_eq_preimage (x : E) (r : ℝ) : closedBall x r = toEuclidean ⁻¹' Metric.closedBall (toEuclidean x) r :=
  rfl

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