le_glueDist_inr_inl — Mathlib

English

The map Sum.inr from Y to X ⊕ Y is an isometry with respect to the glued metric on the disjoint union.

Русский

Отображение Sum.inr: Y → X ⊕ Y является изометрией для склеенной метрики.

LaTeX

$$$\mathrm{Isometry}(\mathrm{Sum.inr}:Y\to X\oplus Y)$.$$

Lean4

theorem le_glueDist_inr_inl (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (x y) : ε ≤ glueDist Φ Ψ ε (.inr x) (.inl y) := by
  rw [glueDist_comm]; apply le_glueDist_inl_inr

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