mapsTo_emetric_ball — Mathlib

English

If f is an isometry, then it maps the EMetric.ball around x to the EMetric.ball around f(x).

Русский

Если f — изометрия, то она отображает шар ЭМетрики вокруг x в шар вокруг f(x).

LaTeX

$$$Isometry(f) \rightarrow \forall x\,\forall r:\, Sets.MapsTo(f, EMetric.ball(x,r), EMetric.ball(f(x),r))$$$

Lean4

theorem mapsTo_emetric_ball (hf : Isometry f) (x : α) (r : ℝ≥0∞) : MapsTo f (EMetric.ball x r) (EMetric.ball (f x) r) :=
  (hf.preimage_emetric_ball x r).ge

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