Commit 2023-07-21 14:16 ef85ff8b

View on Github →

feat(Data/Finset): Add a few Finset lemmas (#5933) Adds four Finset lemmas:

  • Nonempty.inl and Nonempty.inr - unions with Nonempty sets are Nonempty
  • sup'_mono and inf'_mono - analogues of sup_mono and inf_mono.

Estimated changes

added theorem Finset.Nonempty.inl
added theorem Finset.Nonempty.inr
added theorem Finset.inf'_mono
added theorem Finset.sup'_mono