English
For p ≠ Fin.last n and x ∈ { x ∈ Fin(n+1) | x ≠ p }, the inverse equals (p.castLT(val_lt_last h)).predAbove x.
Русский
Для p ≠ Fin.last n и x ∈ { x ∈ Fin(n+1) | x ≠ p }, обратное равняется (p.castLT(val_lt_last h)).predAbove x.
LaTeX
$$$$ \\forall {n} {p : \\mathrm{Fin}(n+1)} (h : p \\neq \\mathrm{Fin.last}(n)) (x : \\{ x : \\mathrm{Fin}(n+1) \\mid x \\neq p \\}),\\n (\\mathrm{finSuccAboveEquiv}(p)).\\mathrm{symm} x = (p.castLT(\\mathrm{Fin.val\\_lt\\_last}(h))).\\mathrm{predAbove} x. $$$$
Lean4
theorem finSuccAboveEquiv_symm_apply_ne_last {p : Fin (n + 1)} (h : p ≠ Fin.last n) (x : { x : Fin (n + 1) // x ≠ p }) :
(finSuccAboveEquiv p).symm x = (p.castLT (Fin.val_lt_last h)).predAbove x :=
by
rw [← Option.some_inj]
simpa [finSuccAboveEquiv] using finSuccEquiv'_ne_last_apply h x.property
