English
Extend a partial system of bijections to a limit ordinal, obtaining a partial equivalence on Iic i that is compatible with previous data and the limit bijection equivLim.
Русский
Расширить частичную систему биекций до предельного порядка, получив частичное эквивалентность на Iic i, совместимую с предыдущими данными и пределом эквивкиemy.
LaTeX
$$$\\text{pEquivOnLim} : \\mathrm{PEquivOn}(f, equivSucc, i) \\to \\mathrm{PEquivOn}(f, equivSucc, \\mathrm{Iic}\\ i)$$$
Lean4
/-- Glue partial families of bijections at a limit ordinal,
obtaining a partial family over a right-open interval. -/
noncomputable def pEquivOnGlue : PEquivOn f equivSucc (Iio i)
where
equiv :=
(piLTLim (X := fun j ↦ F j ≃ piLT X j) hi).symm
⟨fun j ↦ ((e j).restrict fun _ h ↦ h.le).equiv, fun _ _ h ↦
funext fun _ ↦ pEquivOn_apply_eq ((isLowerSet_Iio _).inter <| isLowerSet_Iio _)⟩
nat j k hj hk h := by rw [piLTLim_symm_apply]; exacts [(e _).nat _ _ _, h.trans_lt (hi.mid _).2.1]
compat
hj :=
have k := hi.mid hj
by rw [piLTLim_symm_apply hi ⟨_, k.2.2⟩ (by exact k.2.1)]; apply (e _).compat
