mapsTo_sphere — Mathlib

English

An isometry maps a sphere to a sphere: f(Sphere(x,r)) ⊆ Sphere(f(x), r).

Русский

Изометрия отображает сферу в сферу: f(Сфера(x,r)) ⊆ Сфера(f(x), r).

LaTeX

$$$Isometry(f) \rightarrow \forall x\,\forall r:\, Sets.MapsTo(f, Metric.sphere(x,r), Metric.sphere(f(x), r))$$$

Lean4

theorem mapsTo_sphere (hf : Isometry f) (x : α) (r : ℝ) : MapsTo f (Metric.sphere x r) (Metric.sphere (f x) r) :=
  (hf.preimage_sphere x r).ge

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