Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-25 13:00 dff0ffd6

View on Github →

refactor(data/finset): fix formatting issues

Estimated changes

Created data/finset/basic.lean

added def finset.card

added theorem finset.card_empty

added theorem finset.card_erase_of_mem

added theorem finset.card_erase_of_not_mem

added theorem finset.card_insert_le

added theorem finset.card_insert_of_mem

added theorem finset.card_insert_of_not_mem

added theorem finset.card_upto

added def finset.empty

added theorem finset.empty_inter

added theorem finset.empty_subset

added theorem finset.empty_union

added theorem finset.eq_empty_of_card_eq_zero

added theorem finset.eq_empty_of_forall_not_mem

added theorem finset.eq_empty_of_subset_empty

added theorem finset.eq_of_mem_singleton

added theorem finset.eq_of_singleton_eq

added theorem finset.eq_of_subset_of_subset

added theorem finset.eq_or_mem_of_mem_insert

added def finset.erase

added theorem finset.erase_empty

added theorem finset.erase_eq_of_not_mem

added theorem finset.erase_insert

added theorem finset.erase_insert_subset

added theorem finset.erase_subset

added theorem finset.erase_subset_erase

added theorem finset.erase_subset_of_subset_insert

added theorem finset.exists_mem_empty_eq

added theorem finset.exists_mem_empty_iff

added theorem finset.exists_mem_insert_eq

added theorem finset.exists_mem_insert_iff

added theorem finset.exists_mem_of_ne_empty

added theorem finset.ext

added theorem finset.forall_mem_empty_eq

added theorem finset.forall_mem_empty_iff

added theorem finset.forall_mem_insert_eq

added theorem finset.forall_mem_insert_iff

added theorem finset.forall_of_forall_insert

added theorem finset.insert.comm

added def finset.insert

added theorem finset.insert_eq

added theorem finset.insert_eq_of_mem

added theorem finset.insert_erase

added theorem finset.insert_erase_subset

added theorem finset.insert_subset_insert

added theorem finset.insert_union

added def finset.inter

added theorem finset.inter_assoc

added theorem finset.inter_comm

added theorem finset.inter_distrib_left

added theorem finset.inter_distrib_right

added theorem finset.inter_empty

added theorem finset.inter_left_comm

added theorem finset.inter_right_comm

added theorem finset.inter_self

added theorem finset.lt_of_mem_upto

added def finset.mem

added theorem finset.mem_empty_eq

added theorem finset.mem_empty_iff

added theorem finset.mem_erase_eq

added theorem finset.mem_erase_iff

added theorem finset.mem_erase_of_ne_of_mem

added theorem finset.mem_insert

added theorem finset.mem_insert_eq

added theorem finset.mem_insert_iff

added theorem finset.mem_insert_of_mem

added theorem finset.mem_inter

added theorem finset.mem_inter_eq

added theorem finset.mem_inter_iff

added theorem finset.mem_list_of_mem

added theorem finset.mem_of_mem_erase

added theorem finset.mem_of_mem_insert_of_ne

added theorem finset.mem_of_mem_inter_left

added theorem finset.mem_of_mem_inter_right

added theorem finset.mem_of_mem_list

added theorem finset.mem_of_subset_of_mem

added theorem finset.mem_or_mem_of_mem_union

added theorem finset.mem_singleton

added theorem finset.mem_singleton_iff

added theorem finset.mem_singleton_of_eq

added theorem finset.mem_to_finset

added theorem finset.mem_to_finset_of_nodup

added theorem finset.mem_union_eq

added theorem finset.mem_union_iff

added theorem finset.mem_union_l

added theorem finset.mem_union_left

added theorem finset.mem_union_r

added theorem finset.mem_union_right

added theorem finset.mem_upto_eq

added theorem finset.mem_upto_iff

added theorem finset.mem_upto_of_lt

added theorem finset.mem_upto_succ_of_mem_upto

added theorem finset.ne_empty_of_card_eq_succ

added theorem finset.ne_of_mem_erase

added theorem finset.not_mem_empty

added theorem finset.not_mem_erase

added theorem finset.pair_eq_singleton

added theorem finset.perm_insert_cons_of_not_mem

added theorem finset.singleton_inter_of_mem

added theorem finset.singleton_inter_of_not_mem

added theorem finset.singleton_ne_empty

added theorem finset.subset.antisymm

added theorem finset.subset.refl

added theorem finset.subset.trans

added def finset.subset

added def finset.subset_aux

added theorem finset.subset_empty_iff

added theorem finset.subset_insert

added theorem finset.subset_insert_iff

added theorem finset.subset_insert_of_erase_subset

added theorem finset.subset_of_forall

added def finset.to_finset

added theorem finset.to_finset_eq_of_nodup

added def finset.to_finset_of_nodup

added def finset.union

added theorem finset.union_assoc

added theorem finset.union_comm

added theorem finset.union_distrib_left

added theorem finset.union_distrib_right

added theorem finset.union_empty

added theorem finset.union_left_comm

added theorem finset.union_right_comm

added theorem finset.union_self

added def finset.upto

added theorem finset.upto_succ

added theorem finset.upto_zero

added def finset

added def nodup_list

added def to_nodup_list

added def to_nodup_list_of_nodup

Modified data/list/set.lean

added theorem list.length_erase_of_not_mem

Modified topology/continuity.lean

deleted theorem is_open_prod

deleted theorem is_open_prod_iff

added theorem is_open_set_prod

Modified topology/real.lean

added theorem continuous_add_rat

added theorem continuous_add_real'

added theorem continuous_add_real

added theorem continuous_neg_rat

added theorem continuous_neg_real

added theorem continuous_sub_real

modified theorem exists_supremum_real

added theorem is_closed_ge

added theorem is_closed_le

added theorem is_closed_le_real

added theorem is_open_gt

added theorem is_open_lt

added theorem is_open_lt_real

added theorem tendsto_add_rat

added theorem tendsto_mul_rat

added theorem tendsto_neg_rat

Deleted topology/topological_structures.lean

deleted theorem continuous_add'

deleted theorem continuous_add

deleted theorem continuous_mul

deleted theorem continuous_neg'

deleted theorem continuous_neg

deleted theorem continuous_sub

deleted theorem dense_or_discrete

deleted theorem is_closed_le

deleted theorem is_open_lt

deleted theorem is_open_lt_fst_snd

deleted theorem order_separated

deleted theorem tendsto_add

deleted theorem tendsto_mul

deleted theorem tendsto_neg

deleted theorem tendsto_sub