# 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 : ] (a : α) (as : List α) :
List.equiv (List.insert a as) (a :: as)
theorem List.union_equiv_append {α : Type u_1} [inst : ] (as : List α) (bs : List α) :
List.equiv (List.union as bs) (as ++ bs)
def List.remove {α : Type u_1} [inst : ] (a : α) :
List αList α
Equations
theorem List.mem_remove_iff {α : Type u_1} [inst : ] {a : α} {b : α} {as : List α} :
b List.remove a as b as b a
theorem List.remove_eq_of_not_mem {α : Type u_1} [inst : ] {a : α} {as : List α} :
¬a asList.remove a as = as
theorem List.mem_of_mem_remove {α : Type u_1} [inst : ] {a : α} {b : α} {as : List α} (h : b List.remove a as) :
b as
def List.card {α : Type u_1} [inst : ] :
List α
Equations
@[simp]
theorem List.card_nil {α : Type u_1} [inst : ] :
= 0
@[simp]
theorem List.card_cons_of_mem {α : Type u_1} [inst : ] {a : α} {as : List α} (h : a as) :
List.card (a :: as) =
@[simp]
theorem List.card_cons_of_not_mem {α : Type u_1} [inst : ] {a : α} {as : List α} (h : ¬a as) :
List.card (a :: as) = + 1
theorem List.card_le_card_cons {α : Type u_1} [inst : ] (a : α) (as : List α) :
List.card (a :: as)
@[simp]
theorem List.card_insert_of_mem {α : Type u_1} [inst : ] {a : α} {as : List α} (h : a as) :
@[simp]
theorem List.card_insert_of_not_mem {α : Type u_1} [inst : ] {a : α} {as : List α} (h : ¬a as) :
theorem List.card_remove_of_mem {α : Type u_1} [inst : ] {a : α} {as : List α} :
a as = List.card (List.remove a as) + 1
theorem List.card_subset_le {α : Type u_1} [inst : ] {as : List α} {bs : List α} :
as bs
theorem List.card_map_le {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (as : List α) :
theorem List.card_map_eq_of_inj_on {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {as : List α} :
List.inj_on f asList.card (List.map f as) =
theorem List.card_eq_of_equiv {α : Type u_1} [inst : ] {as : List α} {bs : List α} (h : List.equiv as bs) :
=
theorem List.card_append_disjoint {α : Type u_1} [inst : ] {as : List α} {bs : List α} :
List.Disjoint as bsList.card (as ++ bs) = +
theorem List.card_union_disjoint {α : Type u_1} [inst : ] {as : List α} {bs : List α} (h : List.Disjoint as bs) :