List.formPerm_cons_cons
theorem List.formPerm_cons_cons :
∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (l : List α),
(x :: y :: l).formPerm = Equiv.swap x y * (y :: l).formPerm
The theorem `List.formPerm_cons_cons` states that for any type `α` with decidable equality and any two elements `x` and `y` of that type `α`, along with a list `l` of elements of the same type `α`, the permutation created by the function `List.formPerm` on a list formed by prepending `x` and `y` to `l` will be equal to the product of the permutation that swaps `x` and `y` and the permutation created by the function `List.formPerm` on the list formed by prepending `y` to `l`. In other words, adding an element to the start of a list and forming a permutation with `List.formPerm` is the same as swapping this element with the second one and then forming a permutation with `List.formPerm` on the new list.
More concisely: For any type `α` with decidable equality, `List.formPerm (x :: y :: l) = List.formPerm y :: x :: List.formPerm l * List.swap x y`, where `::` denotes list concatenation, `*` denotes permutation multiplication, and `List.swap` is the permutation that swaps `x` and `y`.
|
List.support_formPerm_le'
theorem List.support_formPerm_le' :
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), {x | l.formPerm x ≠ x} ≤ ↑l.toFinset
This theorem is stating that for any list `l` of elements of type `α`, where `α` has decidable equality, the set of elements that are not fixed by the permutation formed by `l` (i.e., those `x` for which applying the permutation `List.formPerm l` to `x` does not result in `x`) is a subset of the finset obtained by removing duplicates from `l`. In other words, any element that the permutation `List.formPerm l` moves is an element of the list `l`.
More concisely: For any list `l` of distinct elements of type `α` with decidable equality, the set of elements not fixed by the permutation `List.formPerm l` is a subset of the list `l` without duplicates.
|