toGlue_commute — Mathlib

English

Compatibility of glue maps with base inclusions: the glue left map composed with Φ equals the glue right map composed with Ψ.

Русский

Совместимость квадратов склейки: левая карта склейки после Φ равна правой карте склейки после Ψ.

LaTeX

$$$\mathrm{toGlueL}(h_\Phi,h_\Psi) \circ \Phi = \mathrm{toGlueR}(h_\Phi,h_\Psi) \circ \Psi$$$

Lean4

theorem toGlue_commute (hΦ : Isometry Φ) (hΨ : Isometry Ψ) : toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ :=
  by
  let i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
  let _ := i.toUniformSpace.toTopologicalSpace
  funext
  simp only [comp, toGlueL, toGlueR]
  refine SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 ?_)
  exact glueDist_glued_points Φ Ψ 0 _

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