Commit 2024-11-14 01:17 fd8ae999
View on Github →feat(Data.Set.Finite): add map_finite_iSup, map_finite_iInf (#17952)
These are type-indexed versions of map_finset_sup and map_finset_inf.
Some golfing may be possible by either using directly
Following Ruben's advice: there are actually 4 new lemmas (iInf/iSup/biInf/biSup).map_finset_inf, map_finset_sup or deducing map_finite_iInf from map_finite_iSup, but I did not find any clean solution in these directions.