preimage_closedBall

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometry.preimage_closedBall

English

Another illustration of sphere preimage under isometry.

Русский

Еще одно пояснение предобраза сферы под изометрией.

LaTeX

$$f^{-1}(S(f(x), r)) = S(x, r)$$

Lean4

@[simp]
theorem preimage_closedBall (x : E) (r : ℝ) : f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r :=
  f.isometry.preimage_closedBall x r

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru