Mathlib.Data.List.Card

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

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

source

ink

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

Prop

Equations

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

source

ink

theorem List.equiv_iff_subset_and_subset {α : Type u_1} {as : List α} {bs : List α} :

List.equiv as bs ↔ as ⊆ bs ∧ bs ⊆ as

source

ink

theorem List.insert_equiv_cons {α : Type u_1} [inst : DecidableEq α] (a : α) (as : List α) :

List.equiv (List.insert a as) (a :: as)

source

ink

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

List.equiv (List.union as bs) (as ++ bs)

source

ink

def List.remove {α : Type u_1} [inst : 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

source

ink

theorem List.mem_remove_iff {α : Type u_1} [inst : DecidableEq α] {a : α} {b : α} {as : List α} :

b ∈ List.remove a as ↔ b ∈ as ∧ b ≠ a

source

ink

theorem List.remove_eq_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {as : List α} :

¬a ∈ as → List.remove a as = as

source

ink

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

b ∈ as

source

ink

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

List α → ℕ

Equations

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

source

ink

@[simp]

theorem List.card_nil {α : Type u_1} [inst : DecidableEq α] :

List.card [] = 0

source

ink

@[simp]

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

List.card (a :: as) = List.card as

source

ink

@[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

source

ink

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

List.card as ≤ List.card (a :: as)

source

ink

@[simp]

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

List.card (List.insert a as) = List.card as

source

ink

@[simp]

theorem List.card_insert_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {as : List α} (h : ¬a ∈ as) :

List.card (List.insert a as) = List.card as + 1

source

ink

theorem List.card_remove_of_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {as : List α} :

a ∈ as → List.card as = List.card (List.remove a as) + 1

source

ink

theorem List.card_subset_le {α : Type u_1} [inst : DecidableEq α] {as : List α} {bs : List α} :

as ⊆ bs → List.card as ≤ List.card bs

source

ink

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

List.card (List.map f as) ≤ List.card as

source

ink

theorem List.card_map_eq_of_inj_on {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] {f : α → β} {as : List α} :

List.inj_on f as → List.card (List.map f as) = List.card as

source

ink

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

List.card as = List.card bs

source

ink

theorem List.card_append_disjoint {α : Type u_1} [inst : DecidableEq α] {as : List α} {bs : List α} :

List.Disjoint as bs → List.card (as ++ bs) = List.card as + List.card bs

source

ink

theorem List.card_union_disjoint {α : Type u_1} [inst : DecidableEq α] {as : List α} {bs : List α} (h : List.Disjoint as bs) :

List.card (List.union as bs) = List.card as + List.card bs