Commit 2017-11-30 22:10 f57e59f4

View on Github →

feat(data/analysis): calculations with filters / topologies + misc

Estimated changes

modified theorem finset.prod_bind
added theorem finset.prod_eq_fold
modified theorem finset.prod_image
modified theorem finset.prod_insert
modified theorem finset.prod_sdiff
modified theorem finset.prod_sigma
modified theorem finset.prod_singleton
modified theorem finset.prod_union
modified theorem finset.prod_union_inter
added theorem set.eq_univ_iff_forall
modified theorem set.eq_univ_of_forall
modified theorem set.inter_subset_left
modified theorem set.inter_subset_right
modified theorem set.range_id
deleted theorem set.range_of_surjective
modified theorem set.subset_empty_iff
added theorem set.subset_eq_empty
added theorem set.subset_inter_iff
added theorem set.subset_ne_empty
added theorem iff_iff_eq
added theorem iff_of_eq
added def filter.bind
modified theorem filter.bind_def
modified theorem filter.bind_mono2
modified theorem filter.bind_mono
modified theorem filter.bind_sup
deleted theorem filter.fmap_principal
added theorem filter.map_def
modified theorem filter.mem_bind_sets
modified theorem filter.principal_bind