Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-24 19:09 7c72de2b

View on Github →

feat(topology): add topological structures for groups, ring, and linear orders; add instances for rat and real

Estimated changes

deleted def finset.card
deleted theorem finset.card_empty
deleted theorem finset.card_erase_of_mem
deleted theorem finset.card_insert_le
deleted theorem finset.card_insert_of_mem
deleted theorem finset.card_upto
deleted def finset.empty
deleted theorem finset.empty_inter
deleted theorem finset.empty_subset
deleted theorem finset.empty_union
deleted theorem finset.eq_of_singleton_eq
deleted def finset.erase
deleted theorem finset.erase_empty
deleted theorem finset.erase_insert
deleted theorem finset.erase_subset
deleted theorem finset.erase_subset_erase
deleted theorem finset.ext
deleted theorem finset.insert.comm
deleted def finset.insert
deleted theorem finset.insert_eq
deleted theorem finset.insert_eq_of_mem
deleted theorem finset.insert_erase
deleted theorem finset.insert_union
deleted def finset.inter
deleted theorem finset.inter_assoc
deleted theorem finset.inter_comm
deleted theorem finset.inter_distrib_left
deleted theorem finset.inter_empty
deleted theorem finset.inter_left_comm
deleted theorem finset.inter_right_comm
deleted theorem finset.inter_self
deleted theorem finset.lt_of_mem_upto
deleted def finset.mem
deleted theorem finset.mem_empty_eq
deleted theorem finset.mem_empty_iff
deleted theorem finset.mem_erase_eq
deleted theorem finset.mem_erase_iff
deleted theorem finset.mem_insert
deleted theorem finset.mem_insert_eq
deleted theorem finset.mem_insert_iff
deleted theorem finset.mem_insert_of_mem
deleted theorem finset.mem_inter
deleted theorem finset.mem_inter_eq
deleted theorem finset.mem_inter_iff
deleted theorem finset.mem_list_of_mem
deleted theorem finset.mem_of_mem_erase
deleted theorem finset.mem_of_mem_list
deleted theorem finset.mem_singleton
deleted theorem finset.mem_singleton_iff
deleted theorem finset.mem_to_finset
deleted theorem finset.mem_union_eq
deleted theorem finset.mem_union_iff
deleted theorem finset.mem_union_l
deleted theorem finset.mem_union_left
deleted theorem finset.mem_union_r
deleted theorem finset.mem_union_right
deleted theorem finset.mem_upto_eq
deleted theorem finset.mem_upto_iff
deleted theorem finset.mem_upto_of_lt
deleted theorem finset.ne_of_mem_erase
deleted theorem finset.not_mem_empty
deleted theorem finset.not_mem_erase
deleted theorem finset.pair_eq_singleton
deleted theorem finset.singleton_ne_empty
deleted theorem finset.subset.antisymm
deleted theorem finset.subset.refl
deleted theorem finset.subset.trans
deleted def finset.subset
deleted def finset.subset_aux
deleted theorem finset.subset_empty_iff
deleted theorem finset.subset_insert
deleted theorem finset.subset_insert_iff
deleted theorem finset.subset_of_forall
deleted def finset.to_finset
deleted def finset.union
deleted theorem finset.union_assoc
deleted theorem finset.union_comm
deleted theorem finset.union_distrib_left
deleted theorem finset.union_empty
deleted theorem finset.union_left_comm
deleted theorem finset.union_right_comm
deleted theorem finset.union_self
deleted def finset.upto
deleted theorem finset.upto_succ
deleted theorem finset.upto_zero
deleted def finset
deleted def nodup_list
deleted def to_nodup_list
added theorem is_open_prod
added theorem is_open_prod_iff
deleted theorem is_open_set_prod
deleted theorem continuous_add_rat
deleted theorem continuous_add_real'
deleted theorem continuous_add_real
deleted theorem continuous_neg_rat
deleted theorem continuous_neg_real
deleted theorem continuous_sub_real
modified theorem exists_supremum_real
deleted theorem is_closed_ge
deleted theorem is_closed_le
deleted theorem is_closed_le_real
deleted theorem is_open_gt
deleted theorem is_open_lt
deleted theorem is_open_lt_real
deleted theorem tendsto_add_rat
deleted theorem tendsto_mul_rat
deleted theorem tendsto_neg_rat
added theorem continuous_add'
added theorem continuous_add
added theorem continuous_mul
added theorem continuous_neg'
added theorem continuous_neg
added theorem continuous_sub
added theorem dense_or_discrete
added theorem is_closed_le
added theorem is_open_lt
added theorem is_open_lt_fst_snd
added theorem order_separated
added theorem tendsto_add
added theorem tendsto_mul
added theorem tendsto_neg
added theorem tendsto_sub