Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 13:55 2865d8c2

View on Github →

refactor(data/set/prod): add notation class for set-like product (#11300) This PR adds notation class has_set_prod for product of sets and subobjects. I also add an instance for sets. Later I want to migrate finsets and sub* product to this notation class.

Estimated changes

modified theorem set.image_mul_prod
modified theorem set.finite.prod
modified theorem set.Ici_prod_Ici
modified theorem set.Ici_prod_eq
modified theorem set.Iic_prod_Iic
modified theorem set.Iic_prod_eq
modified theorem set.Union_prod
modified theorem set.Union_prod_const
modified theorem set.prod_Union
modified theorem set.prod_eq_seq
modified theorem set.prod_sUnion
modified theorem set.empty_prod
modified theorem set.exists_prod_set
modified theorem set.forall_prod_set
modified theorem set.fst_image_prod
modified theorem set.fst_image_prod_subset
modified theorem set.image_prod
modified theorem set.image_swap_prod
modified theorem set.insert_prod
modified theorem set.mem_prod
modified theorem set.mem_prod_eq
modified theorem set.mk_mem_prod
modified theorem set.mk_preimage_prod_left
modified theorem set.mk_preimage_prod_right
modified theorem set.nonempty.fst
modified theorem set.nonempty.prod
modified theorem set.nonempty.snd
modified theorem set.preimage_swap_prod
modified theorem set.prod_diff_prod
modified theorem set.prod_empty
modified theorem set.prod_eq
modified theorem set.prod_eq_empty_iff
modified theorem set.prod_insert
modified theorem set.prod_inter_prod
modified theorem set.prod_mk_mem_set_prod_eq
modified theorem set.prod_mono
modified theorem set.prod_nonempty_iff
modified theorem set.prod_preimage_left
modified theorem set.prod_preimage_right
modified theorem set.prod_singleton
modified theorem set.prod_subset_iff
modified theorem set.prod_subset_prod_iff
modified theorem set.prod_union
modified theorem set.prod_univ
modified theorem set.singleton_prod
modified theorem set.snd_image_prod
modified theorem set.snd_image_prod_subset
modified theorem set.union_prod
modified theorem set.univ_prod
modified theorem set.univ_prod_univ
modified theorem region_between_subset
modified theorem Inf_sup_Inf
modified theorem Sup_inf_Sup
modified theorem filter.mem_prod_self_iff
modified theorem filter.prod_def
modified theorem filter.prod_same_eq
modified theorem continuous_map.image_coev
modified theorem is_open_prod_iff
modified theorem is_separated_def'