English
For any p in Z, the distance between the left-embedded p and the right-embedded p in the glued distance equals ε.
Русский
Для любого p∈Z расстояние между левой вставкой Φ(p) и правой вставкой Ψ(p) в glossed distance равно ε.
LaTeX
$$$ glueDist Φ Ψ ε (\mathrm{Sum.inl}(Φ(p))) (\mathrm{Sum.inr}(Ψ(p))) = ε. $$$
Lean4
theorem glueDist_glued_points [Nonempty Z] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (p : Z) :
glueDist Φ Ψ ε (.inl (Φ p)) (.inr (Ψ p)) = ε :=
by
have : ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0 :=
by
have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ => by positivity
refine le_antisymm ?_ (le_ciInf A)
have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
rw [this]
exact ciInf_le ⟨0, forall_mem_range.2 A⟩ p
simp only [glueDist, this, zero_add]
