List.attach.proof_1
theorem List.attach.proof_1 : ∀ {α : Type u_1} (l : List α), ∀ x ∈ l, x ∈ l
This theorem states that for any given type `α` and a list `l` of type `α`, any element `x` that is in the list `l` is indeed in the list `l`. This is essentially a tautology or a self-evident truth, which asserts that any member of a list is a member of that list. In mathematical notation, this would be expressed as "For all `x`, if `x` belongs to `l`, then `x` belongs to `l`".
More concisely: For any list `l` and any element `x` in type `α`, if `x ∈ l`, then `x ∈ l`.
|
List.pmap.proof_3
theorem List.pmap.proof_3 : ∀ {α : Type u_1} {P : α → Prop} (a : α) (l : List α), (∀ a_1 ∈ a :: l, P a_1) → P a := by
sorry
This theorem states that for all types `α`, and for any predicate `p` defined on `α`, given an element `a` of type `α` and a list `l` of elements of type `α`, if the predicate `p` holds for every element in the list formed by prepending `a` to `l`, then the predicate `p` also holds for the element `a`.
More concisely: If a predicate `p` holds for all elements in the list `a :: l`, where `a` is an element of type `α` and `l` is a list of elements of type `α`, then `p` holds for `a`.
|
List.pmap.proof_4
theorem List.pmap.proof_4 :
∀ {α : Type u_1} {P : α → Prop} (a : α) (l : List α), (∀ a_1 ∈ a :: l, P a_1) → ∀ x ∈ l, P x
This theorem states that for any type `α`, any property `p` that applies to elements of type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, if every element in the list `a :: l` (which is the list `l` with `a` added to the front) has property `p`, then for any element `x` in the list `l`, `x` must also have property `p`. In other words, if every element in the list that results from adding `a` to `l` has a certain property, then every element in `l` must also have this property.
More concisely: If `a : α` has property `p` and every element in the list `a :: l` of type `α` has property `p`, then every element `x` in `l` also has property `p`.
|