image_ball

Mathlib.Topology.MetricSpace.Isometry

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

← MathLib Explorer

English

The image of a ball under an isometry is a ball with the image center.

Русский

Образ шара под изометрией – шар с изображенным центром.

LaTeX

$$$ h''\!\operatorname{Ball}(x,r) = \operatorname{Ball}(h(x), r) $$$

Lean4

@[simp]
theorem image_ball (h : α ≃ᵢ β) (x : α) (r : ℝ) : h '' Metric.ball x r = Metric.ball (h x) r := by
  rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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