preimage_closedBall — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem preimage_closedBall (x : ℤ) (r : ℝ) : (↑) ⁻¹' closedBall (x : ℝ) r = closedBall x r :=
  rfl

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