closedBall_zero_eq_preimage_closedBall

English

Similarly, the closed ball at the origin equals the preimage of the metric closed ball: p.closedBall 0 r = p^{-1}(Metric.closedBall 0 r).

Русский

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

LaTeX

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

Lean4

theorem closedBall_zero_eq_preimage_closedBall {r : ℝ} : p.closedBall 0 r = p ⁻¹' Metric.closedBall 0 r := by
  rw [closedBall_zero_eq, preimage_metric_closedBall]

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