Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-16 20:36 d69acdc9

View on Github →

feat(data/finset/powerset): More powerset lemmas (#15387) finset.powerset is injective, and others.

Estimated changes

Modified src/data/finset/powerset.lean

added theorem finset.coe_powerset

modified theorem finset.mem_powerset_self

modified theorem finset.powerset_empty

added theorem finset.powerset_eq_singleton_empty

added theorem finset.powerset_inj

added theorem finset.powerset_injective

added theorem finset.powerset_nonempty

Modified src/data/fintype/basic.lean

added theorem finset.powerset_eq_univ

added theorem finset.powerset_univ