Lists'.of_toList
theorem Lists'.of_toList : ∀ {α : Type u_1} (l : Lists' α true), Lists'.ofList l.toList = l
The theorem `Lists'.of_toList` states that for any type `α` and any `ZFA prelist` `l` of type `α`, when we convert `l` to a `List` of `ZFA lists` using the function `Lists'.toList` and then convert it back to a `ZFA prelist` using `Lists'.ofList`, we get `l` back. In other words, the functions `Lists'.toList` and `Lists'.ofList` are inverses of each other when moving from `ZFA prelists` to `Lists` of `ZFA lists` and back.
More concisely: For any type `α` and any `ZFA prelist` `l` of type `α`, the functions `Lists'.ofList (Lists'.toList l)` and `l` are equal.
|
Lists'.mem_of_subset'
theorem Lists'.mem_of_subset' :
∀ {α : Type u_1} {a : Lists α} {l₁ l₂ : Lists' α true}, l₁ ⊆ l₂ → a ∈ l₁.toList → a ∈ l₂
The theorem `Lists'.mem_of_subset'` states that for any type `α`, any ZFA list `a` of type `α`, and any two proper ZFA prelists `l₁` and `l₂` of type `α`, if `l₁` is a subset of `l₂`, and `a` is an element in the list obtained by converting `l₁` to a list of ZFA lists, then `a` is an element of `l₂`. In other words, if a ZFA list is in the list version of a proper ZFA prelist, and that prelist is also a subset of another one, then that ZFA list is also in the larger prelist.
More concisely: If `l₁` is a proper ZFA prelist that is a subset of another proper ZFA prelist `l₂`, and `a` is an element of the list obtained from `l₁`, then `a` is an element of `l₂`.
|
Lists'.cons_subset
theorem Lists'.cons_subset :
∀ {α : Type u_1} {a : Lists α} {l₁ l₂ : Lists' α true}, Lists'.cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂
This theorem states that for any type `α`, any ZFA list `a` of type `α`, and any two proper ZFA prelists `l₁` and `l₂` of type `α`, appending `a` to the front of `l₁` is a subset of `l₂` if and only if `a` is an element of `l₂` and `l₁` is a subset of `l₂`. In other words, the ZFA list `a` and the prelist `l₁` must both be subsets of, or included in, the prelist `l₂` for the operation of appending `a` to `l₁` to result in a prelist that is also a subset of `l₂`.
More concisely: For any type `α`, ZFA list `a` of type `α`, and proper ZFA prelists `l₁` and `l₂` of type `α`, if `a ∈ l₂` and `l₁ ⊆ l₂`, then `a :: l₁ ⊆ l₂`, where `::` denotes the operation of appending an element to the front of a list.
|