Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-18 14:42 cab0481e

View on Github →

feat(data/finset/lattice): mem_sup, mem_sup' (#7245) Sets with bot and closed under sup are closed under finset.sup, and variations for inf, sup', and inf'.

Estimated changes