Cardinality of Lists

This is a makeshift theory of the cardinality of a list. Any list can be taken to represent the finite set of its elements. Cardinality counts the number of distinct elements. Cardinality respects equivalence and is preserved by any mapping that is injective on its elements.

It might make sense to remove this when we have a proper theory of finite sets.

def List.inj_on {α : Type u_1} {β : Sort u_2} (f : α → β) (as : List α) : Prop

Equations

• List.inj_on f as = ∀ {x y : α}, x ∈ as → y ∈ as → f x = f y → x = y

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) : List.inj_on f as

def List.equiv {α : Type u_1} (as : List α) (bs : List α) : Prop

Equations

• List.equiv as bs = ∀ (x : α), x ∈ as ↔ x ∈ bs

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} [DecidableEq α] (a : α) (as : List α) : List.equiv (List.insert a as) (a :: as)

theorem List.union_equiv_append {α : Type u_1} [DecidableEq α] (as : List α) (bs : List α) : List.equiv (as ∪ bs) (as ++ bs)

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

Equations

• List.remove a [] = []
• List.remove a (b :: bs) = if a = b then List.remove a bs else b :: List.remove a bs

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

theorem List.remove_eq_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {as : List α} : ¬a ∈ as → List.remove a as = as

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

def List.card {α : Type u_1} [DecidableEq α] : List α → ℕ

Equations

• List.card [] = 0
• List.card (b :: bs) = if b ∈ bs then List.card bs else List.card bs + 1

@[simp]

theorem List.card_nil {α : Type u_1} [DecidableEq α] : List.card [] = 0

@[simp]

theorem List.card_cons_of_mem {α : Type u_1} [DecidableEq α] {a : α} {as : List α} (h : a ∈ as) : List.card (a :: as) = List.card as

@[simp]

theorem List.card_cons_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {as : List α} (h : ¬a ∈ as) : List.card (a :: as) = List.card as + 1

theorem List.card_le_card_cons {α : Type u_1} [DecidableEq α] (a : α) (as : List α) : List.card as ≤ List.card (a :: as)

@[simp]

theorem List.card_insert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {as : List α} (h : a ∈ as) : List.card (List.insert a as) = List.card as

@[simp]

theorem List.card_insert_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {as : List α} (h : ¬a ∈ as) : List.card (List.insert a as) = List.card as + 1

theorem List.card_remove_of_mem {α : Type u_1} [DecidableEq α] {a : α} {as : List α} : a ∈ as → List.card as = List.card (List.remove a as) + 1

theorem List.card_subset_le {α : Type u_1} [DecidableEq α] {as : List α} {bs : List α} : as ⊆ bs → List.card as ≤ List.card bs

theorem List.card_map_le {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α → β) (as : List α) : List.card (List.map f as) ≤ List.card as

theorem List.card_map_eq_of_inj_on {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α → β} {as : List α} : List.inj_on f as → List.card (List.map f as) = List.card as

theorem List.card_eq_of_equiv {α : Type u_1} [DecidableEq α] {as : List α} {bs : List α} (h : List.equiv as bs) : List.card as = List.card bs

theorem List.card_append_disjoint {α : Type u_1} [DecidableEq α] {as : List α} {bs : List α} : List.Disjoint as bs → List.card (as ++ bs) = List.card as + List.card bs

theorem List.card_union_disjoint {α : Type u_1} [DecidableEq α] {as : List α} {bs : List α} (h : List.Disjoint as bs) : List.card (as ∪ bs) = List.card as + List.card bs