Commit 2024-01-06 09:51 4bd6aa25

View on Github →

chore(Data/Finset): drop some Nonempty arguments (#9377)

  • rename Finset.Nonempty.image_iff to Finset.image_nonempty, deprecate the old version;
  • rename Set.nonempty_image_iff to Set.image_nonempty, deprecate the old version;
  • drop unneeded Finset.Nonempty arguments here and there;
  • add versions of some lemmas that assume Nonempty s instead of Nonempty (s.image f) or Nonempty (s.map f).

Estimated changes

modified theorem Finset.coe_image
added theorem Finset.image_nonempty
modified theorem Finset.inf'_cons
modified theorem Finset.inf'_insert
modified theorem Finset.inf'_map
modified theorem Finset.inf'_singleton
modified theorem Finset.le_sup'
modified theorem Finset.sup'_cons
modified theorem Finset.sup'_insert
deleted theorem Finset.sup'_le
modified theorem Finset.sup'_le_iff
modified theorem Finset.sup'_map
modified theorem Finset.sup'_singleton
modified theorem Finset.inv_nonempty_iff
added theorem Set.image_nonempty
deleted theorem Set.nonempty_image_iff