Documentation

Mathlib.Data.List.Card

def List.inj_on {α : Type u_1} {β : Sort u_2} (f : αβ) (as : List α) :
Equations
theorem List.inj_on_of_subset {α : Type u_1} {β : Sort u_2} {f : αβ} {as : List α} {bs : List α} (h : List.inj_on f bs) (hsub : as bs) :
def List.equiv {α : Type u_1} (as : List α) (bs : List α) :
Equations
theorem List.equiv_iff_subset_and_subset {α : Type u_1} {as : List α} {bs : List α} :
List.equiv as bs as bs bs as
theorem List.insert_equiv_cons {α : Type u_1} [inst : DecidableEq α] (a : α) (as : List α) :
List.equiv (List.insert a as) (a :: as)
theorem List.union_equiv_append {α : Type u_1} [inst : DecidableEq α] (as : List α) (bs : List α) :
List.equiv (List.union as bs) (as ++ bs)
def List.remove {α : Type u_1} [inst : DecidableEq α] (a : α) :
List αList α
Equations
theorem List.mem_remove_iff {α : Type u_1} [inst : DecidableEq α] {a : α} {b : α} {as : List α} :
b List.remove a as b as b a
theorem List.remove_eq_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {as : List α} :
¬a asList.remove a as = as
theorem List.mem_of_mem_remove {α : Type u_1} [inst : DecidableEq α] {a : α} {b : α} {as : List α} (h : b List.remove a as) :
b as
def List.card {α : Type u_1} [inst : DecidableEq α] :
List α
Equations
@[simp]
theorem List.card_nil {α : Type u_1} [inst : DecidableEq α] :
@[simp]
theorem List.card_cons_of_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {as : List α} (h : a as) :
@[simp]
theorem List.card_cons_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {as : List α} (h : ¬a as) :
List.card (a :: as) = List.card as + 1
theorem List.card_le_card_cons {α : Type u_1} [inst : DecidableEq α] (a : α) (as : List α) :
@[simp]
theorem List.card_insert_of_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {as : List α} (h : a as) :
@[simp]
theorem List.card_insert_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {as : List α} (h : ¬a as) :
theorem List.card_remove_of_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {as : List α} :
a asList.card as = List.card (List.remove a as) + 1
theorem List.card_subset_le {α : Type u_1} [inst : DecidableEq α] {as : List α} {bs : List α} :
as bsList.card as List.card bs
theorem List.card_map_le {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] (f : αβ) (as : List α) :
theorem List.card_map_eq_of_inj_on {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] {f : αβ} {as : List α} :
theorem List.card_eq_of_equiv {α : Type u_1} [inst : DecidableEq α] {as : List α} {bs : List α} (h : List.equiv as bs) :
theorem List.card_append_disjoint {α : Type u_1} [inst : DecidableEq α] {as : List α} {bs : List α} :
List.Disjoint as bsList.card (as ++ bs) = List.card as + List.card bs
theorem List.card_union_disjoint {α : Type u_1} [inst : DecidableEq α] {as : List α} {bs : List α} (h : List.Disjoint as bs) :