theorem List.getI_map_range {α : Type u} {i n : ℕ} [Inhabited α] (f : ℕ → α) (h : i < n) : (map f (range n)).getI i = f i

def List.subsetSet {α : Type u} (l : List α) (s : Set α) [DecidablePred s] : Bool

Equations

• l.subsetSet s = List.foldr (fun (a : α) (ih : Bool) => decide (s a) && ih) true l

def List.upper : List ℕ → ℕ

Equations

• [].upper = 0
• (n :: ns).upper = max (n + 1) ns.upper

@[simp]

theorem List.upper_nil : [].upper = 0

@[simp]

theorem List.upper_cons (n : ℕ) (ns : List ℕ) : (n :: ns).upper = max (n + 1) ns.upper

theorem List.lt_upper (l : List ℕ) {n : ℕ} (h : n ∈ l) : n < l.upper

theorem List.toFinset_map {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (l : List α) : (map f l).toFinset = Finset.image f l.toFinset

theorem List.toFinset_mono {α : Type u} [DecidableEq α] {l l' : List α} (h : l ⊆ l') : l.toFinset ⊆ l'.toFinset

def List.sup {α : Type u} [SemilatticeSup α] [OrderBot α] : List α → α

Equations

• [].sup = ⊥
• (a :: as).sup = a ⊔ as.sup

@[simp]

theorem List.sup_nil {α : Type u} [SemilatticeSup α] [OrderBot α] : [].sup = ⊥

@[simp]

theorem List.sup_cons {α : Type u} [SemilatticeSup α] [OrderBot α] (a : α) (as : List α) : (a :: as).sup = a ⊔ as.sup

theorem List.le_sup {α : Type u} [SemilatticeSup α] [OrderBot α] {a : α} {l : List α} : a ∈ l → a ≤ l.sup

theorem List.sup_ofFn {α : Type u} [SemilatticeSup α] [OrderBot α] {n : ℕ} (f : Fin n → α) : (ofFn f).sup = Finset.univ.sup f

theorem List.ofFn_get_eq_map_cast {α : Type u} {β : Type v} {n : ℕ} (g : α → β) (as : List α) {h : n = as.length} : (ofFn fun (i : Fin n) => g (as.get (Fin.cast h i))) = map g as

theorem List.append_subset_append {α : Type u_1} {l₁ l₂ l : List α} (h : l₁ ⊆ l₂) : l₁ ++ l ⊆ l₂ ++ l

theorem List.subset_of_eq {α : Type u_1} {l₁ l₂ : List α} (e : l₁ = l₂) : l₁ ⊆ l₂

def List.remove {α : Type u_1} [DecidableEq α] (a : α) : List α → List α

Equations

• List.remove a = List.filter fun (x : α) => decide (x ≠ a)

@[simp]

theorem List.remove_nil {α : Type u_1} [DecidableEq α] (a : α) : remove a [] = []

@[simp]

theorem List.eq_remove_cons {α : Type u_1} [DecidableEq α] {ψ : α} {l : List α} : remove ψ (ψ :: l) = remove ψ l

@[simp]

theorem List.remove_singleton_of_ne {α : Type u_1} [DecidableEq α] {φ ψ : α} (h : φ ≠ ψ) : remove ψ [φ] = [φ]

theorem List.mem_remove_iff {α : Type u_1} [DecidableEq α] {a b : α} {l : List α} : b ∈ remove a l ↔ b ∈ l ∧ b ≠ a

theorem List.mem_of_mem_remove {α : Type u_1} [DecidableEq α] {a b : α} {l : List α} (h : b ∈ remove a l) : b ∈ l

@[simp]

theorem List.remove_cons_self {α : Type u_1} [DecidableEq α] (l : List α) (a : α) : remove a (a :: l) = remove a l

theorem List.remove_cons_of_ne {α : Type u_1} [DecidableEq α] (l : List α) {a b : α} (ne : a ≠ b) : remove b (a :: l) = a :: remove b l

@[simp]

theorem List.remove_subset {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : remove a l ⊆ l

@[simp]

theorem List.subset_cons_remove {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : l ⊆ a :: remove a l

theorem List.remove_subset_remove {α : Type u_1} [DecidableEq α] (a : α) {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : remove a l₁ ⊆ remove a l₂

theorem List.remove_cons_subset_cons_remove {α : Type u_1} [DecidableEq α] (a b : α) (l : List α) : remove b (a :: l) ⊆ a :: remove b l

theorem List.remove_map_substet_map_remove {α : Type u_2} {β : Type u_1} [DecidableEq α] [DecidableEq β] (f : α → β) (l : List α) (a : α) : remove (f a) (map f l) ⊆ map f (remove a l)

theorem List.induction_with_singleton {F : Type u_1} {motive : List F → Prop} (hnil : motive []) (hsingle : ∀ (a : F), motive [a]) (hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)) (as : List F) : motive as

def List.induction_with_singleton' {α : Type u_2} {motive : List α → Sort u_1} (hnil : motive []) (hsingle : (a : α) → motive [a]) (hcons : (a b : α) → (as : List α) → motive (b :: as) → motive (a :: b :: as)) (as : List α) : motive as

Equations

• List.induction_with_singleton' hnil hsingle hcons [] = hnil
• List.induction_with_singleton' hnil hsingle hcons [a] = hsingle a
• List.induction_with_singleton' hnil hsingle hcons (a :: b :: as) = hcons a b as (List.induction_with_singleton' hnil hsingle hcons (b :: as))

instance List.Nodup.finite {α : Type u_1} [Finite α] : Finite { l : List α // l.Nodup }

theorem List.suffix_of_cons_suffix {α : Type u_1} {l₁ l₂ : List α} {a : α} : a :: l₁ <:+ l₂ → l₁ <:+ l₂

theorem List.suffix_cons_of {α : Type u_1} {l₁ l₂ : List α} {a : α} : l₁ <:+ l₂ → l₁ <:+ a :: l₂

theorem List.exists_of_not_suffix {α : Type u_1} (l₁ l₂ : List α) : ¬l₁ <:+ l₂ → ∃ (l : List α) (a : α), a :: l <:+ l₁ ∧ l <:+ l₂ ∧ ¬a :: l <:+ l₂

theorem List.IsSuffix.eq_or_cons_suffix {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ → l₁ = l₂ ∨ ∃ (a : α✝), a :: l₁ <:+ l₂

theorem List.suffix_trichotomy {α : Type u_1} {l₁ l₂ : List α} (h₁₂ : ¬l₁ <:+ l₂) (h₂₁ : ¬l₂ <:+ l₁) : ∃ (l : List α) (a : α) (b : α), a ≠ b ∧ a :: l <:+ l₁ ∧ b :: l <:+ l₂

theorem List.Vector.get_mk_eq_get {α : Type u_1} {n : ℕ} (l : List α) (h : l.length = n) (i : Fin n) : get ⟨l, h⟩ i = l.get (Fin.cast ⋯ i)

theorem List.Vector.get_one {α : Type u_2} {n : ℕ} (v : Vector α (n + 2)) : v.get 1 = v.tail.head

theorem List.Vector.ofFn_vecCons {α : Type u_1} {n : ℕ} (a : α) (v : Fin n → α) : ofFn (a :> v) = a ::ᵥ ofFn v

theorem List.Vector.cons_get {α : Type u_1} {k : ℕ} (a : α) (v : Vector α k) : (a ::ᵥ v).get = a :> v.get

theorem List.exists_of_not_nil {α : Type u_1} {l : List α} (hl : l ≠ []) : ∃ (a : α), a ∈ l

theorem List.iff_nil_forall {α : Type u_1} {l : List α} : l = [] ↔ ∀ a ∈ l, a ∈ []

theorem List.nodup_iff_get_ne_get {α : Type u_1} {l : List α} : l.Nodup ↔ ∀ (i j : Fin l.length), i < j → l[i] ≠ l[j]

getElem version of List.nodup_iff_getElem?_ne_getElem?

theorem List.Nodup.infinite_of_infinite {α : Type u_1} : Infinite { l : List α // l.Nodup } → Infinite α

theorem List.exists_of_range {α✝ : Type u_1} {f : ℕ → α✝} {n : ℕ} {a : α✝} (h : a ∈ map f (range n)) : ∃ i < n, a = f i

theorem List.single_suffix_uniq {α : Type u_1} {a b : α} {l : List α} (ha : [a] <:+ l) (hb : [b] <:+ l) : a = b