mem_permutations — Mathlib

English

For s,t Lists α, s ∈ permutations t if and only if s is a permutation of t.

Русский

Для любых списков s,t из α верно: s принадлежит permutations t тогда и только тогда, когда s является перестановкой t.

LaTeX

$$$$s \in permutations\ t \iff s \sim t$$$$

Lean4

@[simp]
theorem mem_permutations {s t : List α} : s ∈ permutations t ↔ s ~ t :=
  ⟨perm_of_mem_permutations, mem_permutations_of_perm_lemma mem_permutationsAux_of_perm⟩

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