map_permutations — Mathlib

English

Let f : α → β and ts ∈ List α. Then applying map (map f) to permutations ts yields the same as permutations of map f ts: map (map f) (permutations ts) = permutations (map f ts).

Русский

Пусть f : α → β и ts ∈ List α. Тогда применение map (map f) к permutations ts эквивалентно permutations (map f ts).

LaTeX

$$$$\operatorname{map}(\operatorname{map} f)(\operatorname{permutations}\ ts) = \operatorname{permutations}(\operatorname{map} f\ ts)$$$$

Lean4

theorem map_permutations (f : α → β) (ts : List α) : map (map f) (permutations ts) = permutations (map f ts) := by
  rw [permutations, permutations, map, map_permutationsAux, map]

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