le_glueDist_inl_inr — Mathlib

English

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

Русский

Отображение Sum.inl: X → X ⊕ Y является изометрией для склеенной метрики на частях раздельного объединения.

LaTeX

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

Lean4

theorem le_glueDist_inl_inr (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (x y) : ε ≤ glueDist Φ Ψ ε (.inl x) (.inr y) :=
  le_add_of_nonneg_left <| Real.iInf_nonneg fun _ => by positivity

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