preimage_ball — Mathlib

English

The metric on ℤ is the restriction of the usual metric from ℝ; the preimage under the inclusion map of a real ball around x equals the intrinsic ball in ℤ around x of radius r.

Русский

Метрика на \mathbb{Z} является ограничением обычной метрики из \mathbb{R}; прообраз шара в \mathbb{R} вокруг точки x под включением равен шару в \mathbb{Z} с радиусом r.

LaTeX

$$$(\uparrow)^{-1} B_{\mathbb{R}}(x,r)=B_{\mathbb{Z}}(x,r)$$$

Lean4

theorem preimage_ball (x : ℤ) (r : ℝ) : (↑) ⁻¹' ball (x : ℝ) r = ball x r :=
  rfl

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