Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-02 14:23 5e022925

View on Github →

feat(data/finset/*): Diverse lemmas (#10388) A bunch of simple lemmas

Estimated changes

Modified src/analysis/box_integral/basic.lean

Modified src/data/finset/basic.lean

added theorem finset.filter_bUnion

added theorem finset.sdiff_erase

added theorem finset.subset_erase

Modified src/data/finset/lattice.lean

added theorem finset.inf_comm

added theorem finset.inf_product_left

added theorem finset.inf_product_right

added theorem finset.inf_sigma

added theorem finset.sup_comm

added theorem finset.sup_product_left

added theorem finset.sup_product_right

added theorem finset.sup_sigma

Modified src/data/finset/prod.lean

added theorem finset.coe_product

added theorem finset.product_eq_bUnion_right

Modified src/data/fintype/basic.lean

modified theorem finset.univ_eq_empty

added theorem finset.univ_unique

deleted theorem univ_is_empty

added theorem univ_option

deleted theorem univ_unique

Modified src/data/nat/interval.lean

added theorem finset.range_add_eq_union

added theorem finset.range_image_pred_top_sub

deleted theorem nat.range_image_pred_top_sub

Modified src/data/set/basic.lean

added theorem set.univ_unique

Modified src/geometry/euclidean/monge_point.lean

Modified src/linear_algebra/basis.lean