Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 12:47 f99af7da

View on Github →

chore(data/set/lattice): Generalize more / lemmas to dependent families (#11516) The "bounded union" and "bounded intersection" are both instances of nested /. But they only apply when the inner one runs over a predicate p : ι → Prop, and the resulting set couldn't depend on p. This generalizes to κ : ι → Sort* and allows dependence on κ i. The lemmas are renamed from bUnion/bInter to Union₂/Inter₂ to show that they are more general. Some generalizations lead to unification problems, so I've kept the b version around. Some lemmas were missing between and or between / and nested /, so I'm adding them as well. Renames

Estimated changes

modified theorem set.Inter_congr
added theorem set.Inter_mono'
added theorem set.Inter_mono
deleted theorem set.Inter_subset_Inter2
deleted theorem set.Inter_subset_Inter
modified theorem set.Inter_subset_of_subset
added theorem set.Inter₂_congr
added theorem set.Inter₂_mono'
added theorem set.Inter₂_mono
added theorem set.Inter₂_subset
modified theorem set.Union_Inter_subset
modified theorem set.Union_congr
added theorem set.Union_mono'
added theorem set.Union_mono
modified theorem set.Union_prod_const
modified theorem set.Union_range_eq_Union
added theorem set.Union_set_of
modified theorem set.Union_subset
deleted theorem set.Union_subset_Union2
deleted theorem set.Union_subset_Union
modified theorem set.Union_subset_iff
added theorem set.Union₂_congr
added theorem set.Union₂_inter
added theorem set.Union₂_mono'
added theorem set.Union₂_mono
added theorem set.Union₂_subset
deleted theorem set.bInter_congr
deleted theorem set.bInter_eq_empty_iff
deleted theorem set.bInter_mono'
modified theorem set.bInter_mono
deleted theorem set.bUnion_congr
deleted theorem set.bUnion_eq_univ_iff
deleted theorem set.bUnion_inter
modified theorem set.bUnion_mono
deleted theorem set.bUnion_prod_const
deleted theorem set.bUnion_subset
deleted theorem set.bUnion_subset_Union
deleted theorem set.bUnion_subset_bUnion
added theorem set.compl_Inter₂
added theorem set.compl_Union₂
deleted theorem set.compl_bInter
deleted theorem set.compl_bUnion
added theorem set.image_Union₂
deleted theorem set.image_bInter_subset
deleted theorem set.image_bUnion
added theorem set.inter_Union₂
deleted theorem set.inter_bUnion
added theorem set.maps_to_Inter₂
added theorem set.maps_to_Union₂
deleted theorem set.maps_to_bInter
deleted theorem set.maps_to_bInter_bInter
deleted theorem set.maps_to_bUnion
deleted theorem set.maps_to_bUnion_bUnion
modified theorem set.mem_Inter
modified theorem set.mem_Inter_of_mem
modified theorem set.mem_Inter₂
modified theorem set.mem_Union
added theorem set.mem_Union_of_mem
modified theorem set.mem_Union₂
added theorem set.nonempty_Inter₂
deleted theorem set.nonempty_bInter
modified theorem set.preimage_Inter
added theorem set.preimage_Inter₂
modified theorem set.preimage_Union
added theorem set.preimage_Union₂
deleted theorem set.preimage_bInter
deleted theorem set.preimage_bUnion
modified theorem set.prod_Union
added theorem set.prod_Union₂
deleted theorem set.prod_bUnion
modified theorem set.subset_Inter_iff
added theorem set.subset_Inter₂
added theorem set.subset_Union₂
deleted theorem set.subset_bInter
deleted theorem set.subset_subset_Union
added theorem set.surj_on_Union₂
deleted theorem set.surj_on_bUnion
deleted theorem set.surj_on_bUnion_bUnion