permutations_take_two — Mathlib

English

For any x,y and s, the first two permutations of x :: y :: s are x :: y :: s and y :: x :: s.

Русский

Для любых x, y и s первые две перестановки x :: y :: s равны x :: y :: s и y :: x :: s.

LaTeX

$$$ (x :: y :: s).permutations.take 2 = [x :: y :: s, y :: x :: s] $$$

Lean4

theorem permutations_take_two (x y : α) (s : List α) : (x :: y :: s).permutations.take 2 = [x :: y :: s, y :: x :: s] :=
  by induction s <;> simp [permutations]

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