English
The maps toInductiveLimit commute with the connecting maps f n: toInductiveLimit I (n+1) ∘ f n = toInductiveLimit I n.
Русский
Отображения toInductiveLimit commute с переходами f_n: toInductiveLimit I(n+1) ∘ f_n = toInductiveLimit I(n).
LaTeX
$$$\mathrm{toInductiveLimit}(I, n+1) \circ f_n = \mathrm{toInductiveLimit}(I, n)$$$
Lean4
/-- The maps `toInductiveLimit n` are compatible with the maps `f n`. -/
theorem toInductiveLimit_commute (I : ∀ n, Isometry (f n)) (n : ℕ) :
toInductiveLimit I n.succ ∘ f n = toInductiveLimit I n :=
by
let h := inductivePremetric I
let _ := h.toUniformSpace.toTopologicalSpace
funext x
simp only [comp, toInductiveLimit]
refine SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 ?_)
change inductiveLimitDist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0
rw [inductiveLimitDist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ, leRecOn_self, leRecOn_succ, leRecOn_self, dist_self]
· rfl
· rfl
· exact le_succ _
