Tuple.succAbove_sort_comp_succAbove_eq
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Tuple_succAbove_sort_comp_succAbove_eqLean source · statement
theorem _root_.Tuple.succAbove_sort_comp_succAbove_eq
{n : ℕ} {ι : Type*} [LinearOrder ι] (u : Fin (n + 1) → ι) (hu : Function.Injective u) (i : Fin
(n + 1)) (k : Fin n) :
i.succAbove (Tuple.sort (u ∘ i.succAbove) k) = Tuple.sort u (((Tuple.sort u).symm i).succAbove
k)