mapsTo_closedBall — Mathlib

English

An isometry maps a closed ball to a closed ball: f(ClosedBall(x,r)) ⊆ ClosedBall(f(x), r).

Русский

Изометрия отображает замкнутый шар в замкнутый шар.

LaTeX

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

Lean4

theorem mapsTo_closedBall (hf : Isometry f) (x : α) (r : ℝ) :
    MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) r) :=
  (hf.preimage_closedBall x r).ge

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