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

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)

## 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.remove_eq_of_not_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{as : List α}
:

¬a ∈ as → List.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

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

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

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 α}
:

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

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 α}
:

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