Commit 2023-09-28 12:57 94638cdb

View on Github →

feat: Order isomorphism between Finset α and Set α (#7375) over a fintype. Also fix the name of Finset.mem_powerset_len_univ_iff (it should be powersetLen, not powerset_len).

Estimated changes

Modified Mathlib/Data/Finset/Slice.lean

Modified Mathlib/Data/Fintype/Basic.lean

added theorem Finset.compl_ssubset_compl

added theorem Finset.compl_subset_compl

added theorem Finset.inter_eq_univ

modified theorem Finset.inter_univ

added theorem Finset.subtype_eq_univ

added theorem Finset.subtype_univ

modified theorem Finset.univ_inter

added theorem Fintype.coe_finsetEquivSet

added theorem Fintype.coe_finsetOrderIsoSet

added theorem Fintype.coe_finsetOrderIsoSet_symm

modified theorem Fintype.finsetEquivSet_apply

modified theorem Fintype.finsetEquivSet_symm_apply

Modified Mathlib/Data/Fintype/Powerset.lean

added theorem Finset.filter_subset_univ

added theorem Finset.mem_powersetLen_univ

deleted theorem Finset.mem_powerset_len_univ_iff

modified theorem Finset.powerset_eq_univ

modified theorem Finset.powerset_univ

modified theorem Finset.univ_filter_card_eq

Modified Mathlib/Order/BooleanAlgebra.lean

added theorem compl_lt_compl_iff_lt

Modified Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric.lean