English
Within a successor step of the inductive construction, the new partial equivalence respects the predecessor constraints along the lt relation.
Русский
В пределах перехода по ступени перехода индуктивного построения новое частичное эквивалентность сохраняет ограничения по отношению lt.
LaTeX
$$$\\text{pEquivOnSucc}\\; \\text{...} \\; \\text{...} \\; \\Rightarrow \\; \\text{...}$$$
Lean4
/-- Extend a partial family of bijections by one step. -/
def pEquivOnSucc [InverseSystem f] (hi : ¬IsMax i) (e : PEquivOn f equivSucc (Iic i))
(H : ∀ ⦃i⦄ (hi : ¬IsMax i) x, (equivSucc hi x).1 = f (le_succ i) x) : PEquivOn f equivSucc (Iic i⁺)
where
equiv := piEquivSucc e.equiv (equivSucc hi) hi
nat := isNatEquiv_piEquivSucc hi (H hi) e.nat
compat hsj hj
x := by
obtain eq | lt := hsj.eq_or_lt
· cases (succ_eq_succ_iff_of_not_isMax hj hi).mp eq; simp [piEquivSucc]
· rwa [piEquivSucc, piSplitLE_lt, e.compat]
