List.Subperm.trans
theorem List.Subperm.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁.Subperm l₂ → l₂.Subperm l₃ → l₁.Subperm l₃ := by
sorry
The theorem `List.Subperm.trans` states that for any type `α` and any three lists `l₁`, `l₂`, and `l₃` of that type, if `l₁` is a subpermutation of `l₂` and `l₂` is a subpermutation of `l₃`, then `l₁` is a subpermutation of `l₃`. The relation "subpermutation" (`List.Subperm`) in this context refers to `l₁` being a sublist of a permutation of `l₂`. This theorem is essentially stating the transitivity of the subpermutation relation for lists.
More concisely: If `l₁` is a subpermutation of `l₂` and `l₂` is a subpermutation of `l₃`, then `l₁` is a subpermutation of `l₃`.
|
List.Perm.length_eq
theorem List.Perm.length_eq : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → l₁.length = l₂.length
This theorem states that for all types `α` and for any two lists `l₁` and `l₂` of type `α`, if `l₁` is a permutation of `l₂`, then the length of `l₁` is equal to the length of `l₂`. This means that any rearrangement of the elements in a list does not change its length.
More concisely: If `α` is a type and `l₁` and `l₂` are lists of type `α` such that `l₁` is a permutation of `l₂`, then the lengths of `l₁` and `l₂` are equal.
|
List.perm_iff_count
theorem List.perm_iff_count :
∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ : List α},
l₁.Perm l₂ ↔ ∀ (a : α), List.count a l₁ = List.count a l₂
This theorem, `List.perm_iff_count`, states that for any type `α` with decidable equality and any two lists `l₁` and `l₂` of type `α`, `l₁` is a permutation of `l₂` if and only if for every element `a` of type `α`, the count of `a` in `l₁` is equal to the count of `a` in `l₂`. In other words, two lists are permutations of each other if and only if every element appears the same number of times in both lists.
More concisely: For any type `α` with decidable equality, lists `l₁` and `l₂` of type `α`, the lists are permutations of each other if and only if the count of each element in `l₁` equals the count of that element in `l₂`.
|
List.Perm.subperm
theorem List.Perm.subperm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → l₁.Subperm l₂
This theorem states that for any type `α` and any two lists `l₁` and `l₂` of that type, if `l₁` is a permutation of `l₂`, then `l₁` is a sub-permutation of `l₂`. In other words, if `l₁` can be rearranged to get `l₂`, then `l₁` is a sublist of some permutation of `l₂`. This is analogous to saying that `l₁` is a subset of `l₂`, but with respect to the multiplicities of the elements, and is used to represent the "less than or equal to" relation on multisets.
More concisely: If `l₁` is a permutation of `l₂`, then `l₁` is a sublist of some permutation of `l₂`.
|
List.Perm.filterMap
theorem List.Perm.filterMap :
∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) {l₁ l₂ : List α},
l₁.Perm l₂ → (List.filterMap f l₁).Perm (List.filterMap f l₂)
This theorem states that for any two lists `l₁` and `l₂` of elements of type `α`, and a function `f` mapping elements of type `α` to an `Option` of type `β`, if `l₁` and `l₂` are permutations of each other, then the lists obtained by applying `f` to each element of `l₁` and `l₂` and filtering the `Some` results (i.e., `List.filterMap f l₁` and `List.filterMap f l₂`) are also permutations of each other.
More concisely: If `l₁` and `l₂` are permutations of each other, then `List.filterMap (fun x => f x) l₁` and `List.filterMap (fun x => f x) l₂` are permutations of each other.
|
List.Perm.refl
theorem List.Perm.refl : ∀ {α : Type u_1} (l : List α), l.Perm l
This theorem states that for any given list `l` of an arbitrary type `α`, the list `l` is a permutation of itself. In a more mathematical language, it asserts the reflexivity of the permutation relation over lists, i.e., every list is a permutation of itself, irrespective of the type of elements it contains.
More concisely: For any list `l` of type `α`, `l` is a permutation of itself. (Equivalently, the reflexive property holds for the permutation relation on lists.)
|
List.Perm.eq_singleton
theorem List.Perm.eq_singleton : ∀ {α : Type u_1} {a : α} {l : List α}, l.Perm [a] → l = [a]
This theorem, `List.Perm.eq_singleton`, asserts that for any type `α`, any element `a` of this type, and any list `l` of `α`, if the list `l` is a permutation of the singleton list `[a]`, then `l` must be equal to `[a]`. This is effectively saying that if a list is a permutation of a singleton list, it must be the same singleton list, because there's only one way to permute a single element.
More concisely: Given any type `α`, any element `a` of type `α`, and any list `l` of length 1 in `α`, if `l` is a permutation of the singleton list `[a]`, then `l = [a]`.
|
List.Perm.pairwise_iff
theorem List.Perm.pairwise_iff :
∀ {α : Type u_1} {R : α → α → Prop},
(∀ {x y : α}, R x y → R y x) → ∀ {l₁ l₂ : List α}, l₁.Perm l₂ → (List.Pairwise R l₁ ↔ List.Pairwise R l₂)
This theorem states that for any type `α` and a relation `R` on `α` that is symmetric (i.e., if `R x y` holds, then `R y x` also holds for any `x` and `y` of type `α`), if two lists `l₁` and `l₂` of type `α` are permutations of each other, then the property of pairwise `R` relation holds in `l₁` if and only if it also holds in `l₂`. Here, a list is said to satisfy the pairwise `R` relation if every pair of distinct elements in the list are related by `R`.
More concisely: For any symmetric relation R on type α and permutation l₁, l₂ of lists of elements of α, the property of pairwise relatedness by R holds in l₁ if and only if it holds in l₂.
|
List.Perm.map
theorem List.Perm.map :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) {l₁ l₂ : List α}, l₁.Perm l₂ → (List.map f l₁).Perm (List.map f l₂)
The theorem `List.Perm.map` states that for any two lists `l₁` and `l₂` of type `α` and a function `f` that maps from `α` to `β`, if `l₁` and `l₂` are permutations of each other, then the lists resulting from mapping `f` to each element of `l₁` and `l₂` are also permutations of each other. In other words, applying the same function to each element of two lists that are permutations of each other will yield two new lists that are also permutations of each other.
More concisely: If `l₁` and `l₂` are permutations of each other, then `map f l₁` and `map f l₂` are also permutations of each other for any function `f` from type `α` to type `β`.
|
List.Perm.insert
theorem List.Perm.insert :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) {l₁ l₂ : List α},
l₁.Perm l₂ → (List.insert a l₁).Perm (List.insert a l₂)
This theorem states that for any type `α` with a decidable equality and any two lists `l₁` and `l₂` of this type, if `l₁` and `l₂` are permutations of each other, then the lists obtained by inserting the same element `a` of type `α` into `l₁` and `l₂` (without duplication) are also permutations of each other. Here, `List.Perm` denotes the permutation relationship between two lists, and `List.insert` represents the operation of inserting an element into a list without duplication.
More concisely: If `α` is a type with decidable equality and `l₁` and `l₂` are permutations of each other, then the lists `List.insert a l₁` and `List.insert a l₂` are also permutations of each other.
|
List.Perm.rfl
theorem List.Perm.rfl : ∀ {α : Type u_1} {l : List α}, l.Perm l
The theorem `List.Perm.rfl` states that for all types `α` and for any list `l` of type `α`, the list `l` is permutationally identical to itself. In other words, the order of elements in the list `l` can be rearranged to form the list `l` itself, which is a trivial case of a permutation because it involves no rearrangement.
More concisely: For all types α and lists l of length n over α, the list l is a permutation of itself. (Note: This statement assumes the standard definition of list permutations in Lean, which may differ from standard mathematical definitions depending on context.)
|
List.Perm.nodup_iff
theorem List.Perm.nodup_iff : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → (l₁.Nodup ↔ l₂.Nodup)
The theorem `List.Perm.nodup_iff` states that for any two lists `l₁` and `l₂` of a certain type `α`, if `l₁` is a permutation of `l₂`, then `l₁` has no duplicates if and only if `l₂` has no duplicates. In other words, the property of a list having no duplicates is preserved under permutations.
More concisely: For lists `l₁` and `l₂` of type `α`, if `l₁` is a permutation of `l₂`, then `l₁` has no duplicates if and only if `l₂` has no duplicates.
|
List.Perm.append_right
theorem List.Perm.append_right :
∀ {α : Type u_1} {l₁ l₂ : List α} (t₁ : List α), l₁.Perm l₂ → (l₁ ++ t₁).Perm (l₂ ++ t₁)
This theorem states that for any type `α` and any lists `l₁`, `l₂`, and `t₁` of this type, if `l₁` is a permutation of `l₂`, then the list formed by appending `t₁` to `l₁` is a permutation of the list formed by appending `t₁` to `l₂`. In other words, if two lists are permutations of each other, appending the same list to both will not change this fact.
More concisely: If `l₁` is a permutation of `l₂`, then appending `t` to both `l₁` and `l₂` results in lists that are permutations of each other. (In Lean notation: `permutation l₁ l₂ → list.append _ _ l₁ = list.append _ _ l₂`)
|
List.perm_singleton
theorem List.perm_singleton : ∀ {α : Type u_1} {a : α} {l : List α}, l.Perm [a] ↔ l = [a]
This theorem states that for all types `α`, elements `a` of type `α`, and lists `l` of type `α`, the list `l` is a permutation of the single-element list `[a]` if and only if `l` is identical to the single-element list `[a]`. In other words, a list is a permutation of a singleton list if and only if it is equal to that singleton list.
More concisely: For all types `α` and elements `a` of type `α`, the list `[a]` is a permutation of list `l` of type `α` if and only if `l = [a]`.
|
List.Nodup.perm_iff_eq_of_sublist
theorem List.Nodup.perm_iff_eq_of_sublist :
∀ {α : Type u_1} {l₁ l₂ l : List α}, l.Nodup → l₁.Sublist l → l₂.Sublist l → (l₁.Perm l₂ ↔ l₁ = l₂)
This theorem states that for all lists `l`, `l₁`, and `l₂` of any type `α`, if `l` has no duplicate elements (`List.Nodup l`), and `l₁` and `l₂` are both sublists of `l` (`List.Sublist l₁ l` and `List.Sublist l₂ l`), then `l₁` is a permutation of `l₂` (`List.Perm l₁ l₂`) if and only if `l₁` is equal to `l₂` (`l₁ = l₂`). Essentially, this means that when dealing with sublists of a list with no duplicates, the only way for two such sublists to be permutations of each other is for them to be identical.
More concisely: For lists `l`, `l₁`, and `l₂` of any type `α` with no duplicate elements (`List.Nodup l`), if `l₁` and `l₂` are both sublists of `l` (`List.Sublist l₁ l` and `List.Sublist l₂ l`), then `l₁` is a permutation of `l₂` (`List.Perm l₁ l₂`) if and only if `l₁ = l₂`.
|
List.Subperm.subset
theorem List.Subperm.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Subperm l₂ → l₁ ⊆ l₂
The theorem `List.Subperm.subset` states that for any type `α` and any two lists `l₁` and `l₂` of that type, if `l₁` is a sub-permutation of `l₂` (denoted as `l₁ <+~ l₂`), then all elements of `l₁` are also elements of `l₂`. In other words, `l₁` is a subset of `l₂` (denoted as `l₁ ⊆ l₂`). This theorem establishes a relationship between the sub-permutation and subset properties of two lists.
More concisely: For any type `α` and lists `l₁` and `l₂` of that type, if `l₁` is a sub-permutation of `l₂` (`l₁ <+~ l₂`), then `l₁` is a subset of `l₂` (`l₁ ⊆ l₂`).
|
List.Perm.append_left
theorem List.Perm.append_left : ∀ {α : Type u_1} {t₁ t₂ : List α} (l : List α), t₁.Perm t₂ → (l ++ t₁).Perm (l ++ t₂)
This theorem states that for any type `α`, and any lists `t₁`, `t₂`, and `l` of this type, if `t₁` is a permutation of `t₂`, then the list obtained by appending `t₁` to `l` is a permutation of the list obtained by appending `t₂` to `l`. In mathematical terms, if $t₁$ and $t₂$ are permutations of each other, then $l ∘ t₁$ and $l ∘ t₂$ are also permutations of each other, where $∘$ denotes the concatenation of lists.
More concisely: If `α` is any type and `t₁` and `t₂` are permutations of each other, then the list `l ++ t₁` and `l ++ t₂` are permutations of each other, where `++` denotes list concatenation.
|
List.Perm.countP_eq
theorem List.Perm.countP_eq :
∀ {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α}, l₁.Perm l₂ → List.countP p l₁ = List.countP p l₂
This theorem states that for any type `α`, any predicate function `p` from `α` to `Bool`, and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a permutation of `l₂`, then the number of elements in `l₁` that satisfy the predicate `p` (`List.countP p l₁`) is equal to the number of elements in `l₂` that satisfy the same predicate (`List.countP p l₂`). In other words, rearranging the elements of a list doesn't change the number of elements that satisfy a given predicate.
More concisely: For any type `α`, predicate function `p` from `α` to `Bool`, and lists `l₁` and `l₂` of type `α` that are permutations of each other, `List.countP p l₁` equals `List.countP p l₂`.
|
List.perm_ext_iff_of_nodup
theorem List.perm_ext_iff_of_nodup :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Nodup → l₂.Nodup → (l₁.Perm l₂ ↔ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂)
This theorem, `List.perm_ext_iff_of_nodup`, states that for any two lists `l₁` and `l₂` of a certain type `α`, if both `l₁` and `l₂` do not contain any duplicate elements (i.e., `List.Nodup l₁` and `List.Nodup l₂` are true), then `l₁` is a permutation of `l₂` if and only if any element `a` of type `α` is in `l₁` if and only if `a` is in `l₂`. In other words, two lists without duplicates are permutations of each other if they contain exactly the same elements.
More concisely: For lists `l₁` and `l₂` of type `α` without duplicate elements, `l₁` is a permutation of `l₂` if and only if they have the same elements.
|
List.subperm_cons
theorem List.subperm_cons : ∀ {α : Type u_1} (a : α) {l₁ l₂ : List α}, (a :: l₁).Subperm (a :: l₂) ↔ l₁.Subperm l₂ := by
sorry
The theorem `List.subperm_cons` states that for any type `α`, any element `a` of type `α`, and any lists `l₁` and `l₂` of type `α`, the list `a :: l₁` is a sub-permutation of the list `a :: l₂` if and only if `l₁` is a sub-permutation of `l₂`. Here, a sub-permutation is defined as a sublist of a permutation of another list. This theorem implies that the sub-permutation relation between `a :: l₁` and `a :: l₂` is determined by the sub-permutation relation between `l₁` and `l₂`, irrespective of the element `a`.
More concisely: For any type `α`, lists `l₁` and `l₂` of type `α`, and element `a` of type `α`, the lists `a :: l₁` and `a :: l₂` are sub-permutations of each other if and only if `l₁` is a sub-permutation of `l₂`.
|
List.Perm.erase
theorem List.Perm.erase :
∀ {α : Type u_1} [inst : DecidableEq α] (a : α) {l₁ l₂ : List α}, l₁.Perm l₂ → (l₁.erase a).Perm (l₂.erase a) := by
sorry
This theorem states that for any type `α` with decidable equality, and any element `a` of this type, if two lists `l₁` and `l₂` of elements of type `α` are permutations of each other, then the lists resulting from erasing the element `a` from `l₁` and `l₂` are also permutations of each other. In other words, the operation of erasing a given element preserves the permutation relation between two lists.
More concisely: For types `α` with decidable equality and any element `a` in `α`, if lists `l₁` and `l₂` of `α` are permutations of each other, then the lists obtained by removing `a` from `l₁` and `l₂` are also permutations of each other.
|
List.Perm.append
theorem List.Perm.append :
∀ {α : Type u_1} {l₁ l₂ t₁ t₂ : List α}, l₁.Perm l₂ → t₁.Perm t₂ → (l₁ ++ t₁).Perm (l₂ ++ t₂)
This theorem states that for any type `α` and any lists `l₁`, `l₂`, `t₁`, `t₂` of this type, if `l₁` is a permutation of `l₂` and `t₁` is a permutation of `t₂`, then the concatenation of `l₁` and `t₁` is a permutation of the concatenation of `l₂` and `t₂`. In mathematical terms, it establishes that permutations are preserved under list concatenation.
More concisely: If `l₁` is a permutation of `l₂` and `t₁` is a permutation of `t₂`, then the concatenation of `l₁` and `t₁` is a permutation of the concatenation of `l₂` and `t₂`. In symbols: `(l₁ ∘ l₃) ∧ (t₁ ∘ t₃) ⟹ (l₁ ++ t₁) ≃ (l₂ ++ t₂)`, where `∘` denotes function composition, `++` denotes list concatenation, and `≃` denotes list isomorphism.
|
List.Perm.filter
theorem List.Perm.filter :
∀ {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α}, l₁.Perm l₂ → (List.filter p l₁).Perm (List.filter p l₂) := by
sorry
The theorem `List.Perm.filter` states that for any type `α`, predicate function `p` that maps an element of `α` to a Boolean, and any two lists `l₁` and `l₂` of type `α`, if `l₁` and `l₂` are permutations of each other (i.e., they contain the same elements but possibly in a different order), then the lists resulting from filtering `l₁` and `l₂` with the predicate function `p` are also permutations of each other. In other words, rearranging the elements of a list does not affect the outcome of filtering that list with a given predicate.
More concisely: If two lists `l₁` and `l₂` of the same type `α` are permutations of each other, then the filtered lists `List.filter p l₁` and `List.filter p l₂` are also permutations of each other for any predicate function `p` on `α`.
|
List.subperm_ext_iff
theorem List.subperm_ext_iff :
∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ : List α},
l₁.Subperm l₂ ↔ ∀ x ∈ l₁, List.count x l₁ ≤ List.count x l₂
This theorem, named `List.subperm_ext_iff`, is about lists in Lean and is an analogue of the `Multiset.le_iff_count` for lists. It takes as input a type `α` with a given decidable equality and two lists `l₁` and `l₂` of this type. The theorem states that `l₁` is a sub-permutation of `l₂` (denoted as `List.Subperm l₁ l₂`) if and only if for every element `x` in `l₁`, the count of `x` in `l₁` is less than or equal to the count of `x` in `l₂`. In other words, `l₁` is a sub-permutation of `l₂` if every element of `l₁` appears in `l₂` at least as many times as it appears in `l₁`.
More concisely: A list `l₁` is a sub-permutation of list `l₂` if and only if for every element `x` in `l₁`, the number of occurrences of `x` in `l₁` is less than or equal to the number of occurrences of `x` in `l₂`.
|
List.Perm.symm
theorem List.Perm.symm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → l₂.Perm l₁
This theorem states that, for any type `α` and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a permutation of `l₂`, then `l₂` is also a permutation of `l₁`. In other words, the permutation relation between two lists is symmetric.
More concisely: For any type `α` and lists `l₁` and `l₂` of type `α`, if `l₁` is a permutation of `l₂`, then `l₂` is a permutation of `l₁`.
|
List.Perm.subset
theorem List.Perm.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → l₁ ⊆ l₂
This theorem states that for any type `α` and any two lists `l₁` and `l₂` of this type, if `l₁` is a permutation of `l₂`, then `l₁` is a subset of `l₂`. Here, the term 'subset' is used in the sense of lists, meaning that every element of `l₁` also appears in `l₂`.
More concisely: If `α` is a type and `l₁` is a permutation of `l₂`, then `l₁ ⊆ l₂` (`l₁` is a subset of `l₂`) in the sense of lists.
|
List.perm_cons_erase
theorem List.perm_cons_erase :
∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α}, a ∈ l → l.Perm (a :: l.erase a)
The theorem `List.perm_cons_erase` states that for any type `α` with decidable equality, for any element `a` of type `α`, and for any list `l` of elements of type `α`, if `a` is an element of `l`, then the list `l` is a permutation of the list obtained by appending `a` to the front of the list `l` with `a` removed. In other words, any list is a permutation of itself with any of its elements moved to the front.
More concisely: For any type `α` with decidable equality and any list `l` of elements of type `α`, if `a` is an element of `l`, then the list `[a] ++ l` and `l` are permutations of each other.
|
List.Perm.subperm_right
theorem List.Perm.subperm_right : ∀ {α : Type u_1} {l₁ l₂ l : List α}, l₁.Perm l₂ → (l₁.Subperm l ↔ l₂.Subperm l) := by
sorry
This theorem states that for any three lists `l₁`, `l₂`, and `l` of any type `α`, if `l₁` is a permutation of `l₂`, then `l₁` is a sublist of a permutation of `l` if and only if `l₂` is a sublist of a permutation of `l`. This is essentially saying that the property of being a sublist of a permutation of another list is preserved under permutation of the lists.
More concisely: For any lists `l₁`, `l₂`, and `l` of type `α`, if `l₁` is a permutation of `l₂`, then `l₁` is a sublist of some permutation of `l` if and only if `l₂` is a sublist of some permutation of `l`.
|
List.Perm.cons_inv
theorem List.Perm.cons_inv : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Perm (a :: l₂) → l₁.Perm l₂ := by
sorry
This theorem states that for any type `α` and any element `a` of type `α`, if a list `l₁` with `a` prefixed is a permutation of another list `l₂` with `a` prefixed, then `l₁` is a permutation of `l₂`. In other words, if two lists are permutations of each other once an identical item is added to the start of each, then they were permutations of each other even before that item was added.
More concisely: If two lists `l₁` and `l₂`, each containing an element `a`, are permutations of each other, then `l₁` is a permutation of `l₂`.
|
List.replicate_perm
theorem List.replicate_perm :
∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, (List.replicate n a).Perm l ↔ List.replicate n a = l
This theorem, `List.replicate_perm`, states that for all types `α`, natural numbers `n`, elements `a` of type α, and lists `l` of type `α`, the list obtained by replicating the element `a` `n` times is a permutation of the list `l` if and only if the replicated list is exactly equal to `l`. In other words, a list of `n` copies of `a` is a permutation of `l` only when it is identical to `l`.
More concisely: For all types α, natural numbers n, elements a of α, and lists l of length n of α, List.replicate a n equals l if and only if l is a permutation of List.repeat a.
|
List.Subperm.refl
theorem List.Subperm.refl : ∀ {α : Type u_1} (l : List α), l.Subperm l
The theorem `List.Subperm.refl` states that for any given list `l` of some type `α`, the list `l` is a sublist of a permutation of itself. This is a reflexive property of the `Subperm` relationship, indicating that any list is considered to be a "sub-permutation" of itself. It aligns with the mathematical idea that every set is a subset of itself.
More concisely: For any list `l` of type `α`, `l` is a sublist of some permutation of itself.
|
List.Perm.mem_iff
theorem List.Perm.mem_iff : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, l₁.Perm l₂ → (a ∈ l₁ ↔ a ∈ l₂)
This theorem states that for any type `α`, any element `a` of type `α`, and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a permutation of `l₂`, then `a` is an element of `l₁` if and only if `a` is an element of `l₂`. In simple terms, if two lists are permutations of each other, then any given element is in the first list if and only if it's also in the second list.
More concisely: If `α` is a type, `a` is an element of `α`, and `l₁` and `l₂` are permutations of each other as lists of `α`, then `a` is an element of `l₁` if and only if `a` is an element of `l₂`.
|
List.cons_subperm_of_not_mem_of_mem
theorem List.cons_subperm_of_not_mem_of_mem :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, a ∉ l₁ → a ∈ l₂ → l₁.Subperm l₂ → (a :: l₁).Subperm l₂
This theorem, `List.cons_subperm_of_not_mem_of_mem`, states that for any type `α`, given an element `a` of type `α` and two lists of type `α` (`l₁` and `l₂`), if `a` is not in `l₁`, `a` is in `l₂`, and `l₁` is a subpermutation of `l₂`, then the list formed by consing `a` to the front of `l₁` is a subpermutation of `l₂`. In other words, adding an element to the first list that is present in the second list but not in the first, does not violate the subpermutation property between the two lists.
More concisely: If `a` is not in `l₁`, `a` is in `l₂`, and `l₁` is a subpermutation of `l₂`, then `a :: l₁` is a subpermutation of `l₂`.
|
List.perm_middle
theorem List.perm_middle : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (l₁ ++ a :: l₂).Perm (a :: (l₁ ++ l₂))
This theorem, `List.perm_middle`, states that for any type `α`, any element `a` of type `α`, and any two lists `l₁` and `l₂` of type `α`, the list formed by appending `a` to the concatenation of `l₁` and `l₂` is a permutation of the list formed by prepending `a` to the concatenation of `l₁` and `l₂`. In other words, regardless of the values of `a`, `l₁`, and `l₂`, placing 'a' anywhere in the list doesn't change its permutation status.
This can be expressed in the mathematical notation as follows: ∀ `α`, `a`, `l₁`, `l₂`, `l₁ ++ a :: l₂` is a permutation of `a :: (l₁ ++ l₂)`.
More concisely: For any type `α`, any element `a` of type `α`, and any two lists `l₁` and `l₂` of type `α`, appending `a` to the concatenation of `l₁` and `l₂` results in a list that is a permutation of the list obtained by prepending `a` to the concatenation of `l₁` and `l₂`.
|
List.perm_comm
theorem List.perm_comm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ ↔ l₂.Perm l₁
This theorem, `List.perm_comm`, is a statement about list permutations in any type `α`. Specifically, it states that for any two lists `l₁` and `l₂` of the same type, the property of `l₁` being a permutation of `l₂` is equivalent to `l₂` being a permutation of `l₁`. In other words, the permutation relation between two lists is commutative.
More concisely: For any lists `l₁` and `l₂` of the same type `α`, `l₁` is a permutation of `l₂` if and only if `l₂` is a permutation of `l₁`.
|
List.Perm.foldl_eq'
theorem List.Perm.foldl_eq' :
∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {l₁ l₂ : List α},
l₁.Perm l₂ →
(∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z : β), f (f z x) y = f (f z y) x) →
∀ (init : β), List.foldl f init l₁ = List.foldl f init l₂
The theorem `List.Perm.foldl_eq'` states that for any types `β` and `α`, and for any function `f` of type `β → α → β`, if two lists `l₁` and `l₂` of type `α` are permutations of each other, then for any `x` and `y` in `l₁`, and for any `z` of type `β`, if the function `f` applied to `z`, `x` and `y` (in that order) is equal to `f` applied to `z`, `y` and `x` (in that order), then the result of folding `f` over `l₁` starting with some initial value `init` of type `β` is equal to the result of folding `f` over `l₂` starting with the same initial value. In terms of mathematics, the theorem is saying that the fold of a function over a list remains the same even if the order of elements in the list is changed, as long as the function satisfies a specific commutation condition.
More concisely: If two lists are permutations of each other and the function used for folding satisfies the commutativity condition `f (z, x) = f (z, y) <-> f (z, y) = f (z, x)`, then folding `f` over the first list starting with an initial value is equal to folding `f` over the second list starting with the same initial value.
|
List.Perm.singleton_eq
theorem List.Perm.singleton_eq : ∀ {α : Type u_1} {a : α} {l : List α}, [a].Perm l → [a] = l
The theorem `List.Perm.singleton_eq` states that for any type `α`, any element `a` of type `α`, and any list `l` of type `α`, if the list containing only `a` is a permutation of `l`, then the list containing only `a` is equal to `l`. In other words, if a single-element list is a permutation of another list, then both lists must be equal.
More concisely: If `a` is an element of type `α` and the list `[a]` is a permutation of list `l` of type `α`, then `[a] = l`.
|
List.subperm_append_diff_self_of_count_le
theorem List.subperm_append_diff_self_of_count_le :
∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ : List α},
(∀ x ∈ l₁, List.count x l₁ ≤ List.count x l₂) → (l₁ ++ l₂.diff l₁).Perm l₂
The theorem `List.subperm_append_diff_self_of_count_le` states that for any types `α`, given two lists `l₁` and `l₂` of type `α` where `α` has decidable equality, if every element `x` in list `l₁` occurs no more times in `l₁` than in `l₂`, then appending `l₁` and the difference between `l₂` and `l₁` results in a list that is a permutation of `l₂`. In other words, if every element in `l₁` occurs at most as often as in `l₂`, then adding those elements from `l₂` that are not in `l₁` to `l₁` rearranges the elements to yield `l₂`.
More concisely: If `α` has decidable equality and for all `x` in `l₁`, the number of occurrences of `x` in `l₁` is less than or equal to the number of occurrences of `x` in `l₂`, then `l₁ ++ (l₂ \ l₁)` is a permutation of `l₂`.
|
List.Perm.eq_nil
theorem List.Perm.eq_nil : ∀ {α : Type u_1} {l : List α}, l.Perm [] → l = []
This theorem states that for any list `l` of a certain type `α`, if `l` is a permutation of an empty list, then `l` must be an empty list itself. This makes sense because the only permutation of an empty list is the empty list itself, thus any list that can be rearranged to match an empty list must also be an empty list.
More concisely: If `α` is a type and `l` is a list of type `α`, then `l` is a permutation of the empty list `[]` if and only if `l` is empty.
|
List.perm_append_comm
theorem List.perm_append_comm : ∀ {α : Type u_1} {l₁ l₂ : List α}, (l₁ ++ l₂).Perm (l₂ ++ l₁)
This theorem states that for all lists `l₁` and `l₂` of any type `α`, concatenating `l₁` and `l₂` in that order is permutation-equivalent to concatenating `l₂` and `l₁` in that order. In other words, appending two lists does not depend on the order of the lists, i.e., `l₁ ++ l₂` is a permutation of `l₂ ++ l₁`.
More concisely: For all lists `l₁` and `l₂` of type `α`, the concatenation of `l₁` and `l₂`, `l₁ ++ l₂`, is permutation-equivalent to the concatenation of `l₂` and `l₁`, `l₂ ++ l₁`.
|
List.Sublist.exists_perm_append
theorem List.Sublist.exists_perm_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∃ l, l₂.Perm (l₁ ++ l)
This theorem states that for any type `α` and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂`, then there exists a list `l` such that `l₂` is a permutation of the concatenation of `l₁` and `l`. In other words, if some elements of `l₁` also appear in `l₂` in the same order, we can rearrange `l₂` such that it starts with `l₁`, followed by some other elements `l`.
More concisely: For any type `α` and lists `l₁`, `l₂` of type `α`, if `l₁` is a sublist of `l₂`, then there exists a list `l` such that `l₂` is a permutation of `l₁ ++ l`.
|
List.perm_inv_core
theorem List.perm_inv_core :
∀ {α : Type u_1} {a : α} {l₁ l₂ r₁ r₂ : List α},
(l₁ ++ a :: r₁).Perm (l₂ ++ a :: r₂) → (l₁ ++ r₁).Perm (l₂ ++ r₂)
This theorem, `List.perm_inv_core`, states that for any type `α` and any element `a` of type `α`, if a list created by concatenating `l₁`, `a`, and `r₁` is a permutation of a list created by concatenating `l₂`, `a`, and `r₂`, then the list created by concatenating `l₁` and `r₁` is a permutation of the list created by concatenating `l₂` and `r₂`. In other words, if two lists differ only by the presence of the same single element, and those lists are permutations of each other, then the lists obtained by removing that element are also permutations of each other.
More concisely: If `l₁ × a × r₁` and `l₂ × a × r₂` are permutations of each other, then `l₁ × r₁` and `l₂ × r₂` are permutations of each other.
|
List.reverse_perm
theorem List.reverse_perm : ∀ {α : Type u_1} (l : List α), l.reverse.Perm l
The theorem `List.reverse_perm` states that for any list `l` of elements of an arbitrary type `α`, the reversed list is a permutation of the original list `l`. In other words, reversing a list doesn't change the multiset of elements it contains; it simply rearranges them.
More concisely: The theorem `List.reverse_perm` asserts that reversing the order of elements in a list preserves its multiset.
|
List.perm_replicate
theorem List.perm_replicate :
∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, l.Perm (List.replicate n a) ↔ l = List.replicate n a
The theorem `List.perm_replicate` states that for any type `α`, natural number `n`, element `a` of type `α`, and list `l` of type `α`, the list `l` is a permutation of `n` copies of `a` (i.e., the list created by `List.replicate n a`) if and only if `l` is equal to the list of `n` copies of `a`. This means that the only way that `l` can be a permutation of `n` copies of `a` is when `l` itself is `n` copies of `a`.
More concisely: For any type `α`, natural number `n`, element `a` of type `α`, and list `l` of type `List α`, `l` is a permutation of `n` copies of `a` if and only if `l` equals `List.replicate n a`.
|
List.Perm.recOnSwap'
theorem List.Perm.recOnSwap' :
∀ {α : Type u_1} {motive : (l₁ l₂ : List α) → l₁.Perm l₂ → Prop} {l₁ l₂ : List α} (p : l₁.Perm l₂),
motive [] [] ⋯ →
(∀ (x : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ h → motive (x :: l₁) (x :: l₂) ⋯) →
(∀ (x y : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ h → motive (y :: x :: l₁) (x :: y :: l₂) ⋯) →
(∀ {l₁ l₂ l₃ : List α} (h₁ : l₁.Perm l₂) (h₂ : l₂.Perm l₃),
motive l₁ l₂ h₁ → motive l₂ l₃ h₂ → motive l₁ l₃ ⋯) →
motive l₁ l₂ p
This is a theorem regarding the inductive properties of list permutations in Lean. It is a variant of the `Perm.recOn` theorem but with a generalized 'swap' case. Specifically, this theorem states that for any lists `l₁`, `l₂` of some type `α` and any permutation `p` from `l₁` to `l₂`, if a property `motive` holds for the base case of two empty lists and is preserved under the operations of adding an element to the start of the lists, swapping the first two elements, and concatenating two lists where each satisfies the property, then the `motive` holds for `l₁` and `l₂`. This theorem allows you to prove properties about all permutations of a list by showing that these properties hold in these specific simpler cases, which then can be combined to cover the general case.
More concisely: If a property is preserved under adding an element to the start, swapping the first two elements, and concatenating two lists where each satisfies the property, then the property holds for all permutations of any list.
|
List.Sublist.subperm
theorem List.Sublist.subperm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.Subperm l₂
The theorem `List.Sublist.subperm` establishes that for any type `α` and any two lists `l₁` and `l₂` of that type, if `l₁` is a sublist of `l₂`, then `l₁` is also a subpermutation of `l₂`. In other words, if every element of `l₁` appears in `l₂` in the same order (which is the definition of a sublist), then we can find a permutation of `l₁` that is a sublist of `l₂`. This is a property connecting sublists and subpermutations in the context of lists.
More concisely: If `l₁` is a sublist of `l₂`, then there exists a permutation of `l₁` that is a sublist of `l₂`.
|
List.Perm.subperm_left
theorem List.Perm.subperm_left : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l₁.Perm l₂ → (l.Subperm l₁ ↔ l.Subperm l₂) := by
sorry
The theorem `List.Perm.subperm_left` states that for any type `α` and any three lists of this type `l`, `l₁`, and `l₂`, if `l₁` is a permutation of `l₂`, then `l` is a sublist of a permutation of `l₁` if and only if `l` is a sublist of a permutation of `l₂`. This theorem is a key property of the 'subperm' relation, which is analogous to the subset relation but takes into account the multiplicities of elements in the lists, and is used for the `≤` relation on multisets.
More concisely: For any type `α`, if `l₁` is a permutation of `l₂`, then `l` is a sublist of a permutation of `l₁` if and only if `l` is a sublist of a permutation of `l₂`.
|