map_finRange_perm — Mathlib

English

For any permutation σ of Fin n, map σ on finRange n yields a permutation of finRange n.

Русский

Для произвольной перестановки σ над Fin n образ finRange n под действием σ создаёт перестановку finRange n.

LaTeX

$$$$ \\text{map }\\sigma\\ (finRange\\ n) \\;\\sim\\; finRange\\ n. $$$$

Lean4

theorem map_finRange_perm {n : ℕ} (σ : Equiv.Perm (Fin n)) : map σ (finRange n) ~ finRange n :=
  by
  rw [perm_ext_iff_of_nodup ((nodup_finRange n).map σ.injective) <| nodup_finRange n]
  simpa [mem_map, mem_finRange] using σ.surjective

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