perm_permutations'_iff — Mathlib

English

For all s,t, permutations' s ~ permutations' t iff s ~ t.

Русский

Для любых s,t: permutations' s ~ permutations' t эквивалентно s ~ t.

LaTeX

$$$$\forall {\alpha}, \; {s,t:\ List\ α},\; s.permutations' ~ t.permutations' \iff s ~ 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'⟩

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