Commit 2024-01-14 17:10 a2fd24f6

View on Github →

feat(Finset/{NAry,Pointwise}): add lemmas about Finset.sup etc (#8950)

Estimated changes

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Lattice.lean

modified theorem Finset.inf'_product_left

modified theorem Finset.inf'_product_right

modified theorem Finset.sup'_product_left

modified theorem Finset.sup'_product_right

Modified Mathlib/Data/Finset/NAry.lean

added theorem Finset.inf'_image₂_left

added theorem Finset.inf'_image₂_right

added theorem Finset.inf_image₂_left

added theorem Finset.inf_image₂_right

added theorem Finset.le_inf'_image₂

added theorem Finset.le_inf_image₂

added theorem Finset.sup'_image₂_le

added theorem Finset.sup'_image₂_left

added theorem Finset.sup'_image₂_right

added theorem Finset.sup_image₂_le

added theorem Finset.sup_image₂_left

added theorem Finset.sup_image₂_right

Modified Mathlib/Data/Finset/Pointwise.lean

modified def Finset.imageOneHom

added theorem Finset.inf'_inv

added theorem Finset.inf'_one

added theorem Finset.inf_div_left

added theorem Finset.inf_div_right

added theorem Finset.inf_inv

added theorem Finset.inf_mul_left

added theorem Finset.inf_mul_right

added theorem Finset.inf_one

added theorem Finset.le_inf_div

added theorem Finset.le_inf_mul

added theorem Finset.max'_one

added theorem Finset.max_one

added theorem Finset.min'_one

added theorem Finset.min_one

added theorem Finset.sup'_inv

added theorem Finset.sup'_one

added theorem Finset.sup_div_le

added theorem Finset.sup_div_left

added theorem Finset.sup_div_right

added theorem Finset.sup_inv

added theorem Finset.sup_mul_le

added theorem Finset.sup_mul_left

added theorem Finset.sup_mul_right

added theorem Finset.sup_one