English
Below a limit ordinal, extending a natural family of bijections yields a natural bijection at the limit. Precisely, piEquivLim provides a natural equivalence between the base system and the limit system under appropriate hypotheses.
Русский
Ниже предела, продолжение естественной семейства биекций образует естественную биективность в пределе. Точно: piEquivLim задаёт естественную эквивалентность между базовой и предельной системами при заданных условиях.
LaTeX
$$$\\text{invLimEquiv} \\, : \\, \\lim f i \\cong \\lim (\\piLTProj i)$$$
Lean4
/-- A natural family of bijections below a limit ordinal
induces a bijection at the limit ordinal. -/
@[simps]
def invLimEquiv : limit f i ≃ limit (piLTProj (X := X)) i
where
toFun t := ⟨fun l ↦ equiv l (t.1 l), fun _ _ h ↦ Eq.symm <| by simp_rw [← t.2 h]; apply nat⟩
invFun t := ⟨fun l ↦ (equiv l).symm (t.1 l), fun _ _ h ↦ (Equiv.eq_symm_apply _).mpr <| by rw [nat, ← t.2 h] <;> simp⟩
left_inv t := by ext; apply Equiv.left_inv
right_inv t := by ext1; ext1; apply Equiv.right_inv
