Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-27 05:25 e7e9f30c

View on Github →

feat(set): preliminaries for Haar measure (#3189) comp_sup_eq_sup_comp is renamed comp_sup_eq_sup_comp_of_is_total and there is a new version that doesn't assume that the order is linear. set.image_injective is renamed function.injective.image_injective (in the same way as the existing function.surjective.preimage_injective). set.image_injective is now an iff.

Estimated changes

added theorem finset.bInter_coe
added theorem finset.bInter_insert
added theorem finset.bInter_inter
added theorem finset.card_union_eq
modified theorem finset.comp_inf_eq_inf_comp
modified theorem finset.comp_sup_eq_sup_comp
added theorem finset.infi_insert
added theorem finset.infi_singleton
added theorem finset.infi_union
added theorem finset.supr_insert
added theorem finset.supr_singleton
modified theorem finset.supr_union
added theorem set.diff_inter_diff
modified theorem set.image_injective
added theorem set.image_surjective
added theorem set.preimage_id'
added theorem set.preimage_injective
added theorem set.preimage_preimage
added theorem set.subset.rfl
added theorem set.disjoint.preimage
added theorem set.disjoint_of_subset
added theorem set.subset_diff
modified theorem function.injective.ne