Commit 2023-12-27 08:00 df4f6559

View on Github →

feat: Finite supremum over a product (#9223) From LeanCamCombi

Estimated changes

Modified Mathlib/Data/Finset/Lattice.lean

added theorem Finset.inf'_prodMap

added theorem Finset.inf_prodMap

added theorem Finset.prodMk_inf'_inf'

added theorem Finset.prodMk_sup'_sup'

added theorem Finset.sup'_prodMap

added theorem Finset.sup_prodMap