English
If two auxiliary bijections and their limits are equal, then piEquivLim yields the same equivalence independent of the particular representatives chosen.
Русский
Если две дополняющих биекции и их пределы равны, то piEquivLim даёт одинаковую эквивалентность независимо от выбранных представителей.
LaTeX
$$$\\text{equivLim} = \\text{equivLim}_1 \\Rightarrow \\forall hi j, \\mathrm{piEquivLim}\\; (nat) \\; (equivLim) = \\mathrm{piEquivLim}\\; (nat)\\; (equivLim_1)\\; hi\\; j$$$
Lean4
theorem unique_pEquivOn (hs : IsLowerSet s) {e₁ e₂ : PEquivOn f equivSucc s} : e₁ = e₂ :=
by
obtain ⟨e₁, nat₁, compat₁⟩ := e₁
obtain ⟨e₂, nat₂, compat₂⟩ := e₂
ext1; ext1 i; dsimp only
refine
SuccOrder.prelimitRecOn i.1 (motive := fun i ↦ ∀ h : i ∈ s, e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩) (fun i nmax ih hi ↦ ?_)
(fun i lim ih hi ↦ ?_) i.2
· ext x ⟨j, hj⟩
obtain rfl | hj := ((lt_succ_iff_of_not_isMax nmax).mp hj).eq_or_lt
· exact (compat₁ _ nmax x).trans (compat₂ _ nmax x).symm
have hi : i ∈ s := hs (le_succ i) hi
rw [piLTProj_intro (f := e₁ _ x) (le_succ i) (by exact hj), ← nat₁ _ hi (by exact le_succ i), ih,
nat₂ _ hi (by exact le_succ i)]
· ext x j
have ⟨k, hjk, hki⟩ := lim.mid j.2
have hk : k ∈ s := hs hki.le hi
rw [piLTProj_intro (f := e₁ _ x) hki.le hjk, piLTProj_intro (f := e₂ _ x) hki.le hjk, ← nat₁ _ hk, ← nat₂ _ hk,
ih _ hki]
