decomposeFin_symm_apply_one — Mathlib

English

For all n, e ∈ Perm(Fin n), p ∈ Fin(n+2), the value at 1 is swap 0 p applied to (e 0).succ.

Русский

Для всех n, e ∈ Perm(Fin n), p ∈ Fin(n+2) значение в 1 равно (swap 0 p) примененному к (e 0).succ.

LaTeX

$$$ \\mathrm{decomposeFin.symm}(p,e)(1) = \\mathrm{swap}(0,p)\\big( (e(0)).\\mathrm{succ} \\big)$$$

Lean4

@[simp]
theorem decomposeFin_symm_apply_one {n : ℕ} (e : Perm (Fin (n + 1))) (p : Fin (n + 2)) :
    Equiv.Perm.decomposeFin.symm (p, e) 1 = swap 0 p (e 0).succ := by
  rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]

Похожие утверждения