Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-08 09:48 bc7d81be

View on Github →

feat(data/{set,finset}/basic): Convenience lemmas (#17957) Add a few convenient corollaries to existing lemmas.

Estimated changes

modified theorem finset.disjoint_val
modified theorem finset.not_subset
modified theorem finset.singleton_inj
added theorem finset.subset_sdiff
added theorem finset.forall_image
added theorem finset.le_inf_const_le
added theorem finset.sup_const_le
added theorem finset.codisjoint_left
added theorem fintype.univ_Prop
deleted theorem set.diff_eq_self
deleted theorem set.disjoint_diff
modified theorem set.disjoint_empty
modified theorem set.disjoint_of_subset
modified theorem set.disjoint_of_subset_left
modified theorem set.disjoint_singleton
modified theorem set.disjoint_singleton_left
modified theorem set.disjoint_union_left
modified theorem set.disjoint_union_right
modified theorem set.disjoint_univ
modified theorem set.empty_disjoint
modified theorem set.subset_diff
modified theorem set.univ_disjoint
modified theorem set.Inter_const
added theorem set.Inter_eq_const
modified theorem set.Union_const
added theorem set.Union_eq_const
added theorem le_sdiff
added theorem sdiff_eq_left
added theorem subset_of_eq_of_subset
added theorem subset_of_subset_of_eq