List.subperm.of_cons
theorem List.subperm.of_cons : ∀ {α : Type u_1} (a : α) {l₁ l₂ : List α}, (a :: l₁).Subperm (a :: l₂) → l₁.Subperm l₂
This theorem, `List.subperm.of_cons`, is essentially an alias for the forward direction of the `List.subperm_cons` theorem. It states that for any type `α` and element `a` of type `α`, along with two lists `l₁` and `l₂` of elements of type `α`, if the list created by appending `a` to the front of `l₁` is a subpermutation of the list created by appending `a` to the front of `l₂`, then `l₁` is a subpermutation of `l₂`.
In mathematical terms, given a type `α`, an element `a` of type `α`, and two lists `l₁` and `l₂` of type `List α`, if `(a :: l₁)` is a subpermutation of `(a :: l₂)`, then we can infer that `l₁` is a subpermutation of `l₂`.
More concisely: If `(a :: l₁)` is a subpermutation of `(a :: l₂)`, then `l₁` is a subpermutation of `l₂`.
|
List.subperm.cons
theorem List.subperm.cons : ∀ {α : Type u_1} (a : α) {l₁ l₂ : List α}, l₁.Subperm l₂ → (a :: l₁).Subperm (a :: l₂) := by
sorry
This theorem, `List.subperm.cons`, is an alias of the reverse direction of `List.subperm_cons`. It states that for any type `α`, any element `a` of type `α`, and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a sub-permutation of `l₂`, then the list formed by prepending `a` to `l₁` is a sub-permutation of the list formed by prepending `a` to `l₂`. Here, a sub-permutation of a list is a list that is obtained by deleting some (possibly zero) elements from the original list.
More concisely: If `l₁` is a sub-permutation of `l₂`, then appending `a` to `l₁` results in a sub-permutation of `a` appended to `l₂`.
|
List.bind_append_perm
theorem List.bind_append_perm :
∀ {α : Type u_1} {β : Type u_2} (l : List α) (f g : α → List β),
(l.bind f ++ l.bind g).Perm (l.bind fun x => f x ++ g x)
The theorem `List.bind_append_perm` states that for any list `l` of elements of some type `α` and any two functions `f` and `g` from `α` to lists of elements of some type `β`, the list resulting from first binding `l` with `f`, then appending the result to the list resulting from binding `l` with `g`, is a permutation of the list resulting from binding `l` with a function that, for each element in `l`, applies `f` to it and appends the result to the result of applying `g` to it. In simpler terms, changing the order in which we append the lists doesn't change the overall list, up to permutation.
More concisely: For any list `l` of type `α`, functions `f: α → βlist` and `g: α → βlist`, the list `(l >>= f) @ (l >>= g)` is a permutation of `(l >>= (λ x => f x @ g x))`.
|