Documentation Verification Report

Powerset

📁 Source: Mathlib/Data/Fintype/Powerset.lean

Statistics

Metric	Count
Definitions `fintype`, `fintype`	2
Theorems `filter_subset_univ`, `mem_powersetCard_univ`, `powerset_eq_univ`, `powerset_univ`, `univ_filter_card_eq`, `card_finset`, `card_finset_len`, `card_set`, `instFinite`	9
Total	11

Finset

Definitions

Name	Category	Theorems
`fintype` 📖	CompOp	17 math math: `Fintype.prod_add`, `ContinuousMultilinearMap.map_add_univ`, `MultilinearMap.map_add_sub_map_add_sub_linearDeriv`, `Fintype.card_finset`, `MultilinearMap.map_add_eq_map_add_linearDeriv_add`, `ContinuousAlternatingMap.map_add_univ`, `Fin.sum_pow_mul_eq_add_pow`, `filter_subset_univ`, `univ_shatters`, `Fintype.card_finset_len`, `Fintype.sum_pow_mul_eq_add_pow`, `MvPolynomial.esymm_eq_sum_subtype`, `powerset_univ`, `univ_filter_card_eq`, `MultilinearMap.map_add_univ`, `shatters_univ`, `powerset_eq_univ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`filter_subset_univ` 📖	mathematical	—	`filter` `Finset` `instHasSubset` `instDecidableRelSubset` `univ` `fintype` `powerset`	—	`ext`
`mem_powersetCard_univ` 📖	mathematical	—	`Finset` `instMembership` `powersetCard` `univ` `card`	—	`mem_powersetCard` `subset_univ`
`powerset_eq_univ` 📖	mathematical	—	`powerset` `univ` `Finset` `fintype`	—	`powerset_univ`
`powerset_univ` 📖	mathematical	—	`powerset` `univ` `Finset` `fintype`	—	`coe_injective` `coe_powerset` `coe_univ` `Set.powerset_univ`
`univ_filter_card_eq` 📖	mathematical	—	`filter` `Finset` `card` `univ` `fintype` `powersetCard`	—	`ext`

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_finset` 📖	mathematical	—	`card` `Finset` `Finset.fintype` `Monoid.toNatPow` `Nat.instMonoid`	—	`Finset.card_powerset`
`card_finset_len` 📖	mathematical	—	`card` `Finset` `Finset.card` `Subtype.fintype` `Finset.fintype` `Nat.choose`	—	`subtype_card` `Finset.univ_filter_card_eq` `Finset.card_powersetCard`
`card_set` 📖	mathematical	—	`card` `Set` `Set.fintype` `Monoid.toNatPow` `Nat.instMonoid`	—	`Finset.card_map` `Finset.card_powerset`

Set

Definitions

Name	Category	Theorems
`fintype` 📖	CompOp	3 math math: `Fintype.card_set`, `fintypeToFinBoolAlgOp_map`, `fintypeToFinBoolAlgOp_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFinite` 📖	mathematical	—	`Finite` `Set`	—	`nonempty_fintype` `Finite.of_fintype`

---

← Back to Index