Commit 2021-05-04 02:29 5a91d05e

View on Github →

feat(data/finset/lattice): add sup_image (#7428) This also renames finset.map_sup to finset.sup_map to match finset.sup_insert and finset.sup_singleton. The inf versions are added too.

Estimated changes

Modified src/data/finset/fold.lean

added theorem finset.fold_image_idem

Modified src/data/finset/lattice.lean

added theorem finset.inf_image

added theorem finset.inf_map

deleted theorem finset.map_inf

deleted theorem finset.map_sup

added theorem finset.sup_image

added theorem finset.sup_map