ball_zero_eq_preimage_ball — Mathlib

English

For any r, the ball at the origin with radius r equals the preimage of the metric ball of radius r around 0 under p: p.ball 0 r = p^{-1}(Metric.ball 0 r).

Русский

Шар вокруг нуля радиуса r равен предобразу метрического шара радиуса r вокруг 0: p.ball 0 r = p^{-1}(Metric.ball 0 r).

LaTeX

$$$p.ball 0 r = p^{-1}(\mathrm{Metric.ball} 0 r)$$$

Lean4

theorem ball_zero_eq_preimage_ball {r : ℝ} : p.ball 0 r = p ⁻¹' Metric.ball 0 r := by
  rw [ball_zero_eq, preimage_metric_ball]

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