This file contains auxiliary results for lists without duplicates (which have the Nodup property).
theorem
List.length_eq_of_nodup_of_same_elements
{α : Type u_1}
[DecidableEq α]
(as bs : List α)
(nodup_as : as.Nodup)
(nodup_bs : bs.Nodup)
(same_elems : ∀ (e : α), e ∈ as ↔ e ∈ bs)
:
If two lists have no duplicates and have the same elements, then their length is the same. Note that the lists are not necessarily equal since the order of elements may differ.
theorem
List.length_le_of_nodup_of_subset
{α : Type u_1}
[DecidableEq α]
(as bs : List α)
(nodup : as.Nodup)
(subset : as ⊆ bs)
:
If a list is duplicate free and the sublist of another list, then the second list is at least as long as the first.
theorem
List.equiv_of_nodup_of_length_eq_of_subset
{α : Type u_1}
[DecidableEq α]
(as bs : List α)
(nodup : as.Nodup)
(eq_length : as.length = bs.length)
(subset : as ⊆ bs)
(e : α)
:
If a list is duplicate free and the sublist of another list that has the same length, then both lists have exactly the same elements.