Yet another simple theorem

Using Rocq
2

Hi!

Here is how I would approach it.

  1. for any lists L1, L2 and a function f, Permutation L1 L2 -> Permutation (map f L1) (map f L2).
  2. for any list L of length n, L = map (fun i => nth i L 0) (seq 0 n).
  3. let f i = nth i L1 0, and write L1 ~ L2 for Permutation L1 L2. Then
    map f L2 ~ map f (seq 0 n) ~ L1 ~ seq 0 n
    (the first ~ is by (1), the second one by (2) and the third one by hypothesis).

Cheers!
Nicolás

1 Like