English
For all m with hx, hy, inductiveLimitDist f x y equals dist between the images in X_m after applying the appropriate transition.
Русский
Для всех m и hx, hy предрасстояние inductiveLimitDist f x y равно расстоянию между образами в X_m после применения соответствующего перехода.
LaTeX
$$$\forall m\, (hx: x.1 \le m)\,(hy: y.1 \le m),\; \nabla\; inductiveLimitDist\, f\, x\, y = \mathrm{dist}(\mathrm{leRecOn}\; hx\; (f\,)\; x.2,\; \mathrm{leRecOn}\; hy\; (f\,)\; y.2) $$$
Lean4
/-- The predistance on the disjoint union `Σ n, X n` can be computed in any `X k` for large
enough `k`. -/
theorem inductiveLimitDist_eq_dist (I : ∀ n, Isometry (f n)) (x y : Σ n, X n) :
∀ m (hx : x.1 ≤ m) (hy : y.1 ≤ m),
inductiveLimitDist f x y = dist (leRecOn hx (f _) x.2 : X m) (leRecOn hy (f _) y.2 : X m)
| 0, hx, hy => by
obtain ⟨i, x⟩ := x; obtain ⟨j, y⟩ := y
obtain rfl : i = 0 := nonpos_iff_eq_zero.1 hx
obtain rfl : j = 0 := nonpos_iff_eq_zero.1 hy
rfl
| (m + 1), hx, hy => by
by_cases h : max x.1 y.1 = (m + 1)
· generalize m + 1 = m' at *
subst m'
rfl
· have : max x.1 y.1 ≤ succ m := by simp [hx, hy]
have : max x.1 y.1 ≤ m := by simpa [h] using of_le_succ this
have xm : x.1 ≤ m := le_trans (le_max_left _ _) this
have ym : y.1 ≤ m := le_trans (le_max_right _ _) this
rw [leRecOn_succ xm, leRecOn_succ ym, (I m).dist_eq]
exact inductiveLimitDist_eq_dist I x y m xm ym
