preimage_ball — Mathlib

English

For an isometry f, the preimage of a ball is the corresponding ball in the domain.

Русский

Для изометрии f прообраз шара равен соответствующему шару в области определения.

LaTeX

$$$Isometry(f) \rightarrow \forall x\, \forall r:\, f^{-1}(\mathrm{Metric.ball}(f(x), r)) = \mathrm{Metric.ball}(x, r)$$$

Lean4

theorem preimage_ball (hf : Isometry f) (x : α) (r : ℝ) : f ⁻¹' Metric.ball (f x) r = Metric.ball x r :=
  hf.preimage_setOf_dist x (· < r)

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