infDist_image

Mathlib.Topology.MetricSpace.HausdorffDistance

URI: https://scilib.ai/kg/mathlib#Metric.infDist_image

← MathLib Explorer

English

The infimum distance is invariant under isometries (re-statement of infDist_image).

Русский

Инфинум расстояния сохраняется под изометриями.

LaTeX

$$infDist (\Phi x) (\Phi '' t) = infDist x t$$

Lean4

/-- The infimum distance is invariant under isometries. -/
theorem infDist_image (hΦ : Isometry Φ) : infDist (Φ x) (Φ '' t) = infDist x t := by simp [infDist, infEdist_image hΦ]

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

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

Разделы

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

Аффилиация

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