isometry_optimalGHInjl — Mathlib

English

The injection of X into the optimal coupling is an isometry.

Русский

Инъекция X в оптимальном связывании является изометрией.

LaTeX

$$Isometry (optimalGHInjl X Y)$$

Lean4

/-- The injection of `X` in the optimal coupling between `X` and `Y` is an isometry. -/
theorem isometry_optimalGHInjl : Isometry (optimalGHInjl X Y) :=
  Isometry.of_dist_eq fun _ _ => candidates_dist_inl (optimalGHDist_mem_candidatesB X Y) _ _

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