perm_permutations_iff — Mathlib

English

For all s,t, permutations s ~ permutations t iff s ~ t; this is the symmetric form of the previous result.

Русский

Для любых s,t, permutations s ~ permutations t эквивалентно s ~ t; это симметричная форма предыдущей идеи.

LaTeX

$$$$\text{Permutations } s \sim \text{Permutations } t \iff s \sim t$$$$

Lean4

@[simp]
theorem perm_permutations_iff {s t : List α} : permutations s ~ permutations t ↔ s ~ t :=
  ⟨fun h => mem_permutations.1 <| h.mem_iff.1 <| mem_permutations.2 (Perm.refl _), Perm.permutations⟩

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