Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-05 14:15 ba95269a

View on Github →

feat(topology): introduce infinite sums on topological monoids

Estimated changes

added theorem finset.prod_bind
added theorem finset.prod_comm
added theorem finset.prod_product
added theorem finset.prod_subset
added theorem finset.filter_false
added theorem finset.filter_filter
added theorem finset.filter_subset
added theorem finset.filter_union
added theorem finset.image_empty
added theorem finset.image_filter
added theorem finset.image_insert
added theorem finset.image_inter
added theorem finset.image_singleton
added theorem finset.image_union
added theorem finset.mem_filter_iff
added theorem finset.mem_image_iff
added theorem finset.mem_sdiff_iff
added theorem finset.subset_inter
added theorem finset.union_subset
deleted def finset
modified def nodup_list
added def {u}
added theorem finset.bind_empty
added theorem finset.bind_image
added theorem finset.bind_insert
added theorem finset.image_bind
added theorem finset.mem_bind_iff
added theorem finset.mem_product_iff
added theorem list.mem_filter_iff
added theorem lattice.infi_top
added theorem lattice.supr_bot
added theorem at_top_ne_bot
added theorem cauchy_iff
added theorem forall_and_distrib'
added def is_sum
added theorem is_sum_add
added theorem is_sum_hom
added theorem is_sum_iff_is_sum
added theorem is_sum_of_is_sum
added theorem is_sum_of_iso
added theorem is_sum_sigma
added theorem is_sum_sum
added theorem is_sum_sum_of_ne_zero
added theorem is_sum_zero
added theorem map_at_top_eq
added theorem mem_at_top_iff
added theorem mem_closure_of_tendsto
added theorem tendsto_add'
added theorem tendsto_sum
added theorem uniform_continuous_add
added theorem uniform_continuous_neg
added theorem uniform_continuous_sub
added theorem uniform_continuous_id