image_ball

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometryEquiv.image_ball

English

The image of a ball under a linear isometry is a ball of the same radius around the image of its center.

Русский

Образ шара линейной изометрией есть шар того же радиуса вокруг образа центра шара.

LaTeX

$$$e''\,\mathsf{Ball}(x,r) = \mathsf{Ball}(e x, r)$$$

Lean4

@[simp]
theorem image_ball (x : E) (r : ℝ) : e '' Metric.ball x r = Metric.ball (e x) r :=
  e.toIsometryEquiv.image_ball x r

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

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

Разделы

Аффилиация

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