isometry_optimalGHInjr — Mathlib

English

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

Русский

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

LaTeX

$$Isometry (optimalGHInjr X Y)$$

Lean4

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

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