Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-07 16:49 aacd7575

View on Github →

feat(measurable_space): more properties of measurable sets in a product (#3703) Add multiple lemmas about prod to set.basic Some cleanup in set.basic Fix the name of the instance measure_space ℝ Cleanup and a couple of additions to the prod section of measurable_space. Rename: prod_singleton_singleton -> singleton_prod_singleton Use prod.swap in the statement of image_swap_prod.

Estimated changes

modified theorem set.diff_self
modified theorem set.image_empty
modified theorem set.image_id'
modified theorem set.image_swap_prod
modified theorem set.mem_prod
modified theorem set.mem_prod_eq
modified theorem set.mk_mem_prod
modified theorem set.prod_empty
modified theorem set.prod_eq
modified theorem set.prod_inter_prod
modified theorem set.prod_mk_mem_set_prod_eq
added theorem set.prod_singleton
added theorem set.prod_union
modified theorem set.set_of_eq_eq_singleton
added theorem set.singleton_prod
added theorem set.union_prod
modified theorem set.univ_prod_univ
modified theorem set.prod_eq_seq
modified theorem is_measurable.prod
added theorem is_measurable_prod
modified theorem measurable.fst
modified theorem measurable.prod
modified theorem measurable.prod_mk
modified theorem measurable.snd
modified theorem measurable_fst
modified theorem measurable_snd