Commit 2021-07-12 11:40 e99f68f5

View on Github →

feat(Data/List/Card): add a theory of cardinality for lists (#25)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

added theorem List.cons_union

added theorem List.mem_filter

added theorem List.mem_filterAux

added theorem List.mem_inter_iff

added theorem List.mem_reverse

added theorem List.mem_reverseAux

added theorem List.mem_union_iff

added theorem List.nil_union

Created Mathlib/Data/List/Card.lean

added def List.card

added theorem List.card_append_disjoint

added theorem List.card_cons_of_mem

added theorem List.card_cons_of_not_mem

added theorem List.card_eq_of_equiv

added theorem List.card_insert_of_mem

added theorem List.card_insert_of_not_mem

added theorem List.card_le_card_cons

added theorem List.card_map_eq_of_inj_on

added theorem List.card_map_le

added theorem List.card_nil

added theorem List.card_remove_of_mem

added theorem List.card_subset_le

added theorem List.card_union_disjoint

added def List.disjoint

added theorem List.equiv_iff_subset_and_subset

added def List.inj_on

added theorem List.inj_on_of_subset

added theorem List.insert_equiv_cons

added theorem List.mem_of_mem_remove

added theorem List.mem_remove_iff

added def List.remove

added theorem List.remove_eq_of_not_mem

added theorem List.union_equiv_append

Modified Mathlib/Logic/Basic.lean

added theorem decide_eq_false_iff_not

added theorem decide_eq_true_iff