English
There exists a canonical bijection between the limit of a directed system and the limit of its projected limit system; this bijection is explicit and natural in the index.
Русский
Существует каноническая биекция между пределом направленной системы и пределом проецируемой предельной системы; биекция явная и естественна по индексу.
LaTeX
$$$\\text{invLimEquiv} : \\lim f i \\cong \\lim (\\piLTProj i)$$$
Lean4
theorem isNatEquiv_piEquivLim [InverseSystem f] (H : ∀ x l, (equivLim x).1 l = f l.2.le x) :
IsNatEquiv f (piEquivLim nat equivLim hi) := fun j k hj hk h t ↦
by
obtain rfl | hj := hj.eq_or_lt
· obtain rfl | hk := hk.eq_or_lt
· simp [InverseSystem.map_self]
· funext l
simp_rw [piEquivLim, piSplitLE_lt hk, piSplitLE_eq, Equiv.trans_apply]
rw [piLTProj, piLTLim_symm_apply hi ⟨k, hk⟩ (by exact l.2), invLimEquiv_apply_coe, H]
· rw [piEquivLim, piSplitLE_lt (h.trans_lt hj), piSplitLE_lt hj]; apply nat
