List.append_cancel_left
theorem List.append_cancel_left : ∀ {α : Type u_1} {as bs cs : List α}, as ++ bs = as ++ cs → bs = cs
This theorem states that for any type `α` and any three lists of that type (`as`, `bs`, and `cs`), if the result of appending `bs` to `as` equals the result of appending `cs` to `as`, then `bs` must equal `cs`. In other words, if we have two equal lists that were formed by appending different lists to the same list, then those different lists must have been equal. This is a property of the list append operation in Lean.
More concisely: If for any type `α`, `as : list α`, `bs, cs : list α`, `as ++ bs = as ++ cs` implies `bs = cs`, then `append` is commutative over lists of type `α`.
|
List.append_cancel_right
theorem List.append_cancel_right : ∀ {α : Type u_1} {as bs cs : List α}, as ++ bs = cs ++ bs → as = cs
This theorem states that for any type `α` and any lists `as`, `bs`, and `cs` of type `α`, if the list obtained by appending `bs` to `as` is the same as the list obtained by appending `bs` to `cs`, then `as` must be equal to `cs`. In other words, if appending the same list `bs` to two lists `as` and `cs` results in the same list, then `as` and `cs` were initially the same list.
More concisely: If for lists `as`, `bs`, and `cs` of type `α`, `as ++ bs` = `cs ++ bs` implies `as` = `cs`, then the theorem states the equivalence of list concatenation and list identity.
|
List.append_cancel_right_eq
theorem List.append_cancel_right_eq : ∀ {α : Type u_1} (as bs cs : List α), (as ++ bs = cs ++ bs) = (as = cs) := by
sorry
This theorem states that for any type `α` and any three lists `as`, `bs`, and `cs` of type `α`, the equivalence of the concatenation of `as` and `bs` with the concatenation of `cs` and `bs` implies that `as` and `cs` are equal. In other words, if appending the same list `bs` to two other lists `as` and `cs` results in the same list, then `as` and `cs` must be the same.
More concisely: If for any lists `as`, `bs`, and `cs` of type `α`, `as ++ bs = cs ++ bs` implies `as = cs`, then the theorem states that list concatenation is commutative and associative up to equality.
|
List.append_cancel_left_eq
theorem List.append_cancel_left_eq : ∀ {α : Type u_1} (as bs cs : List α), (as ++ bs = as ++ cs) = (bs = cs)
This theorem states that for any type `α` and any three lists `as`, `bs`, and `cs` of that type, appending `as` to `bs` results in the same list as appending `as` to `cs` if and only if `bs` is equal to `cs`. In other words, if the concatenation of `as` and `bs` is the same as the concatenation of `as` and `cs`, it implies that the lists `bs` and `cs` must be the same. The theorem is essentially asserting the cancellation law for list concatenation.
More concisely: For any type `α` and lists `as : list α`, `bs`, `cs : list α`, if `as ++ bs` = `as ++ cs`, then `bs` = `cs`. (Here, `++` denotes list concatenation in Lean.)
|
List.ext
theorem List.ext : ∀ {α : Type u_1} {l₁ l₂ : List α}, (∀ (n : ℕ), l₁.get? n = l₂.get? n) → l₁ = l₂
The theorem `List.ext` states that for any type `α`, and for any two lists `l₁` and `l₂` of elements of type `α`, if for every natural number `n`, the `n`-th elements of `l₁` and `l₂` are equal (i.e., `List.get? l₁ n = List.get? l₂ n`), then the two lists `l₁` and `l₂` are equal. This theorem asserts the principle of extensionality for lists, which states that two lists are equal if and only if their corresponding elements are equal.
More concisely: If two lists of the same type have equal elements at every position, then they are equal.
|