Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-08-31 08:51 442a83d7

View on Github →

feat(data/finset/lattice): sup'/inf' lemmas (#18989) Match (most of) the lemmas between finset.sup/finset.inf and finset.sup'/finset.inf'. Also golf two proofs using eq_of_forall_ge_iff to make sure both APIs prove their lemmas in as closely as possible a way. Also define finset.nontrivial to match set.nontrivial.

Estimated changes

modified theorem finset.attach_eq_empty_iff
modified theorem finset.attach_nonempty_iff
added theorem finset.cons_empty
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
modified theorem finset.filter_false_of_mem
modified theorem finset.filter_true
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
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'