Commit 2023-09-09 21:45 b2cf368d

View on Github →

feat: More Finset.sup' lemmas (#7021) Match https://github.com/leanprover-community/mathlib/pull/18989

Estimated changes

modified theorem Finset.attach_eq_empty_iff
modified theorem Finset.attach_nonempty_iff
added theorem Finset.cons_empty
modified theorem Finset.filter_False
modified theorem Finset.filter_True
added theorem Finset.filter_comm
added theorem Finset.filter_const
modified theorem Finset.filter_eq_empty_iff
modified theorem Finset.filter_eq_self
modified theorem Finset.filter_false_of_mem
modified theorem Finset.filter_nonempty_iff
modified theorem Finset.filter_true_of_mem
deleted theorem Finset.sdiff_self
added theorem Finset.inf'_image
added theorem Finset.inf'_sup_inf'
added theorem Finset.inf'_union
modified theorem Finset.inf_biUnion
modified theorem Finset.inf_const
added theorem Finset.inf_ite
modified theorem Finset.inf_top
added theorem Finset.sup'_image
added theorem Finset.sup'_inf_sup'
added theorem Finset.sup'_union
added theorem map_finset_inf'
added theorem map_finset_sup'
deleted theorem Finset.inf'_union
deleted theorem Finset.sup'_union