English
If two limit-based equivalences coincide, then their images on comparable indices coincide as well.
Русский
Если две эквиваленции, основанные на пределе, совпадают, то их изображения на сопоставимых индексах совпадают.
LaTeX
$$$\\mathrm{piEquivLim} \\; nat \\; equivLim = \\mathrm{piEquivLim} \\; nat \\; equivLim_1$$$
Lean4
/-- Extend `pEquivOnGlue` by one step, obtaining a partial family over a right-closed interval. -/
noncomputable def pEquivOnLim [InverseSystem f] (equivLim : F i ≃ limit f i)
(H : ∀ x l, (equivLim x).1 l = f l.2.le x) : PEquivOn f equivSucc (Iic i)
where
equiv := piEquivLim (pEquivOnGlue hi e).nat equivLim hi
nat := isNatEquiv_piEquivLim (pEquivOnGlue hi e).nat hi H
compat hsj hj
x := by
rw [piEquivLim, piSplitLE_lt (hi.succ_lt <| (succ_le_iff_of_not_isMax hj).mp hsj)]
apply (pEquivOnGlue hi e).compat
