English
Define a predistance glueDist on X ⊕ Y depending on basepoint maps Φ, Ψ and ε>0; it matches the actual distance inside each component and uses a glue-distance across the two components leveraging basepoints and ε.
Русский
Определяем предрасстояние glueDist на X ⊕ Y в зависимости от отображений-оснований Φ, Ψ и ε>0; внутри каждой компоненты расстояние обычное, между компонентами применяется glue-дистанция через основания и ε.
LaTeX
$$$ glueDist(\Φ,\Ψ,ε): (X\oplus Y) \to (X\oplus Y) \to \mathbb{R},\quad glueDist(\Sum.inl x,\Sum.inr y)=\big(\inf_p \mathrm{dist}(x,\Φ(p)) + \mathrm{dist}(y,\Ψ(p))\big) + ε, \text{ and similarly for the other cross-pair}. $$$
Lean4
/-- Define a predistance on `X ⊕ Y`, for which `Φ p` and `Ψ p` are at distance `ε` -/
def glueDist (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) : X ⊕ Y → X ⊕ Y → ℝ
| .inl x, .inl y => dist x y
| .inr x, .inr y => dist x y
| .inl x, .inr y => (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ε
| .inr x, .inl y => (⨅ p, dist y (Φ p) + dist x (Ψ p)) + ε
