infEdist_image — Mathlib

English

Infimum distance is invariant under isometries: infEdist (Φ x) (Φ '' t) = infEdist x t whenever Φ is an isometry.

Русский

Инвариантность infEdist под изометриями: infEdist(Φ x) (Φ'' t) = infEdist x t, если Φ — изометрия.

LaTeX

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

Lean4

/-- The infimum edistance is invariant under isometries -/
theorem infEdist_image (hΦ : Isometry Φ) : infEdist (Φ x) (Φ '' t) = infEdist x t := by
  simp only [infEdist, iInf_image, hΦ.edist_eq]

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