Fintype

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

Statistics

Metric	Count
Definitions `ToType`, `cast`, `coeEmbedding`, `coeEquiv`, `consEquiv`, `fintypeCoe`, `instCoeOutToType`, `instCoeSortType`, `instFintypeElemProdNatSetOfLtSndCountFst`, `mapEquiv`, `mapEquiv_aux`, `mkToType`, `toEnumFinset`	13
Theorems `card_coe`, `card_toEnumFinset`, `cast_apply_fst`, `cast_apply_snd`, `cast_symm_apply_fst`, `cast_symm_apply_snd`, `coeEmbedding_apply`, `coeEquiv_apply_coe`, `coeEquiv_symm_apply_fst`, `coeEquiv_symm_apply_snd_val`, `coe_consEquiv_of_eq_of_eq`, `coe_consEquiv_of_eq_of_lt`, `coe_consEquiv_of_ne`, `coe_mem`, `coe_mk`, `consEquiv_symm_none`, `consEquiv_symm_some`, `exists_coe`, `forall_coe`, `image_toEnumFinset_fst`, `instIsEmptyToTypeEmptyCollection`, `instIsEmptyToTypeOfNat`, `mapEquiv_apply`, `map_fst_le_of_subset_toEnumFinset`, `map_toEnumFinset_fst`, `map_univ`, `map_univ_coe`, `map_univ_coeEmbedding`, `map_univ_comp_coe`, `mem_of_mem_toEnumFinset`, `mem_toEnumFinset`, `prod_eq_prod_coe`, `prod_eq_prod_toEnumFinset`, `prod_toEnumFinset`, `sum_eq_sum_coe`, `sum_eq_sum_toEnumFinset`, `sum_toEnumFinset`, `toEmbedding_coeEquiv_trans`, `toEnumFinset_filter_eq`, `toEnumFinset_mono`, `toEnumFinset_subset_iff`	41
Total	54

Multiset

Definitions

Name	Category	Theorems
`ToType` 📖	CompOp	26 math math: `coe_consEquiv_of_eq_of_eq`, `cast_symm_apply_fst`, `coeEquiv_apply_coe`, `sum_toEnumFinset`, `consEquiv_symm_some`, `coeEmbedding_apply`, `prod_eq_prod_coe`, `map_univ_coe`, `map_univ_coeEmbedding`, `cast_apply_fst`, `toEmbedding_coeEquiv_trans`, `coe_consEquiv_of_eq_of_lt`, `map_univ`, `mapEquiv_apply`, `prod_toEnumFinset`, `map_univ_comp_coe`, `cast_symm_apply_snd`, `coeEquiv_symm_apply_fst`, `cast_apply_snd`, `sum_eq_sum_coe`, `consEquiv_symm_none`, `instIsEmptyToTypeOfNat`, `coeEquiv_symm_apply_snd_val`, `coe_consEquiv_of_ne`, `card_coe`, `instIsEmptyToTypeEmptyCollection`
`cast` 📖	CompOp	4 math math: `cast_symm_apply_fst`, `cast_apply_fst`, `cast_symm_apply_snd`, `cast_apply_snd`
`coeEmbedding` 📖	CompOp	4 math math: `coeEquiv_apply_coe`, `coeEmbedding_apply`, `map_univ_coeEmbedding`, `toEmbedding_coeEquiv_trans`
`coeEquiv` 📖	CompOp	4 math math: `coeEquiv_apply_coe`, `toEmbedding_coeEquiv_trans`, `coeEquiv_symm_apply_fst`, `coeEquiv_symm_apply_snd_val`
`consEquiv` 📖	CompOp	5 math math: `coe_consEquiv_of_eq_of_eq`, `consEquiv_symm_some`, `coe_consEquiv_of_eq_of_lt`, `consEquiv_symm_none`, `coe_consEquiv_of_ne`
`fintypeCoe` 📖	CompOp	9 math math: `sum_toEnumFinset`, `prod_eq_prod_coe`, `map_univ_coe`, `map_univ_coeEmbedding`, `map_univ`, `prod_toEnumFinset`, `map_univ_comp_coe`, `sum_eq_sum_coe`, `card_coe`
`instCoeSortType` 📖	CompOp	—
`instFintypeElemProdNatSetOfLtSndCountFst` 📖	CompOp	—
`mapEquiv` 📖	CompOp	1 math math: `mapEquiv_apply`
`mapEquiv_aux` 📖	CompOp	—
`mkToType` 📖	CompOp	1 math math: `coe_mk`
`toEnumFinset` 📖	CompOp	16 math math: `sum_eq_sum_toEnumFinset`, `coeEquiv_apply_coe`, `sum_toEnumFinset`, `toEnumFinset_mono`, `prod_eq_prod_toEnumFinset`, `toEnumFinset_subset_iff`, `map_univ_coeEmbedding`, `mem_toEnumFinset`, `map_toEnumFinset_fst`, `toEmbedding_coeEquiv_trans`, `prod_toEnumFinset`, `coeEquiv_symm_apply_fst`, `card_toEnumFinset`, `coeEquiv_symm_apply_snd_val`, `image_toEnumFinset_fst`, `toEnumFinset_filter_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_coe` 📖	mathematical	—	`Fintype.card` `ToType` `fintypeCoe` `card`	—	`Fintype.card_congr` `Fintype.card_coe` `card_toEnumFinset`
`card_toEnumFinset` 📖	mathematical	—	`Finset.card` `toEnumFinset` `card`	—	`Finset.card.eq_1` `card_map` `map_toEnumFinset_fst`
`cast_apply_fst` 📖	mathematical	—	`count` `DFunLike.coe` `Equiv` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `cast`	—	—
`cast_apply_snd` 📖	mathematical	—	`count` `DFunLike.coe` `Equiv` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `cast`	—	—
`cast_symm_apply_fst` 📖	mathematical	—	`count` `DFunLike.coe` `Equiv` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `cast`	—	—
`cast_symm_apply_snd` 📖	mathematical	—	`count` `DFunLike.coe` `Equiv` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `cast`	—	—
`coeEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `ToType` `Function.instFunLikeEmbedding` `coeEmbedding` `count`	—	—
`coeEquiv_apply_coe` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `toEnumFinset` `DFunLike.coe` `Equiv` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `coeEquiv` `Function.Embedding` `Function.instFunLikeEmbedding` `coeEmbedding`	—	—
`coeEquiv_symm_apply_fst` 📖	mathematical	—	`count` `DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `toEnumFinset` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `coeEquiv`	—	—
`coeEquiv_symm_apply_snd_val` 📖	mathematical	—	`count` `Finset` `SetLike.instMembership` `Finset.instSetLike` `toEnumFinset` `DFunLike.coe` `Equiv` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `coeEquiv`	—	—
`coe_consEquiv_of_eq_of_eq` 📖	mathematical	`count` `cons`	`DFunLike.coe` `Equiv` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `consEquiv`	—	—
`coe_consEquiv_of_eq_of_lt` 📖	mathematical	`count` `cons`	`DFunLike.coe` `Equiv` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `consEquiv`	—	`LT.lt.ne`
`coe_consEquiv_of_ne` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ToType` `cons` `EquivLike.toFunLike` `Equiv.instEquivLike` `consEquiv` `count`	—	—
`coe_mem` 📖	mathematical	—	`Multiset` `instMembership` `count`	—	`count_pos`
`coe_mk` 📖	mathematical	—	`count` `mkToType`	—	—
`consEquiv_symm_none` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ToType` `cons` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `consEquiv` `count` `count_cons_self`	—	—
`consEquiv_symm_some` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ToType` `cons` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `consEquiv` `count` `count_le_count_cons`	—	—
`exists_coe` 📖	mathematical	—	`count`	—	`Sigma.exists`
`forall_coe` 📖	mathematical	—	`count`	—	`Sigma.forall`
`image_toEnumFinset_fst` 📖	mathematical	—	`Finset.image` `toEnumFinset` `toFinset`	—	`Finset.image.eq_1` `map_toEnumFinset_fst`
`instIsEmptyToTypeEmptyCollection` 📖	mathematical	—	`IsEmpty` `ToType` `Multiset` `instEmptyCollection`	—	`Fintype.card_eq_zero_iff` `Fintype.card_eq_zero` `instIsEmptyToTypeOfNat`
`instIsEmptyToTypeOfNat` 📖	mathematical	—	`IsEmpty` `ToType` `Multiset` `instZero`	—	`Fintype.card_eq_zero_iff` `card_coe`
`mapEquiv_apply` 📖	mathematical	—	`count` `map` `DFunLike.coe` `Equiv` `ToType` `EquivLike.toFunLike` `Equiv.instEquivLike` `mapEquiv`	—	—
`map_fst_le_of_subset_toEnumFinset` 📖	mathematical	`Finset` `Finset.instHasSubset` `toEnumFinset`	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `Finset.val`	—	`count_map` `Prod.mk_right_injective` `Finset.singleton_product` `forall_swap` `Mathlib.Tactic.Push.not_and_eq` `Finset.filter.congr_simp` `map_congr` `card_map` `card_range` `Finset.card_mono` `LE.le.trans_lt`
`map_toEnumFinset_fst` 📖	mathematical	—	`map` `Finset.val` `toEnumFinset`	—	`ext'` `count_map` `filter_congr` `Prod.mk_right_injective` `toEnumFinset_filter_eq` `Finset.singleton_product` `map_congr` `card_map` `card_range`
`map_univ` 📖	mathematical	—	`map` `ToType` `count` `Finset.val` `Finset.univ` `fintypeCoe`	—	`map_congr` `map_univ_comp_coe`
`map_univ_coe` 📖	mathematical	—	`map` `ToType` `count` `Finset.val` `Finset.univ` `fintypeCoe`	—	`map_toEnumFinset_fst` `map_congr` `map_map` `map_univ_coeEmbedding`
`map_univ_coeEmbedding` 📖	mathematical	—	`Finset.map` `ToType` `coeEmbedding` `Finset.univ` `fintypeCoe` `toEnumFinset`	—	`Finset.ext`
`map_univ_comp_coe` 📖	mathematical	—	`map` `ToType` `count` `Finset.val` `Finset.univ` `fintypeCoe`	—	`map_map` `map_univ_coe`
`mem_of_mem_toEnumFinset` 📖	mathematical	`Finset` `Finset.instMembership` `toEnumFinset`	`Multiset` `instMembership`	—	`mem_toEnumFinset` `count_pos`
`mem_toEnumFinset` 📖	mathematical	—	`Finset` `Finset.instMembership` `toEnumFinset` `count`	—	`Set.mem_toFinset`
`prod_eq_prod_coe` 📖	mathematical	—	`prod` `Finset.prod` `ToType` `Finset.univ` `fintypeCoe` `count`	—	`map_univ_coe`
`prod_eq_prod_toEnumFinset` 📖	mathematical	—	`prod` `Finset.prod` `toEnumFinset`	—	`map_toEnumFinset_fst`
`prod_toEnumFinset` 📖	mathematical	—	`Finset.prod` `toEnumFinset` `ToType` `Finset.univ` `fintypeCoe` `count`	—	`Fintype.prod_equiv` `Finset.prod_coe_sort`
`sum_eq_sum_coe` 📖	mathematical	—	`sum` `Finset.sum` `ToType` `Finset.univ` `fintypeCoe` `count`	—	`map_univ_coe`
`sum_eq_sum_toEnumFinset` 📖	mathematical	—	`sum` `Finset.sum` `toEnumFinset`	—	`map_toEnumFinset_fst`
`sum_toEnumFinset` 📖	mathematical	—	`Finset.sum` `toEnumFinset` `ToType` `Finset.univ` `fintypeCoe` `count`	—	`Fintype.sum_equiv` `Finset.sum_coe_sort`
`toEmbedding_coeEquiv_trans` 📖	mathematical	—	`Function.Embedding.trans` `ToType` `Finset` `SetLike.instMembership` `Finset.instSetLike` `toEnumFinset` `Equiv.toEmbedding` `coeEquiv` `Function.Embedding.subtype` `coeEmbedding`	—	`Function.Embedding.ext`
`toEnumFinset_filter_eq` 📖	mathematical	—	`Finset.filter` `toEnumFinset` `SProd.sprod` `Finset` `Finset.instSProd` `Finset.instSingleton` `Finset.range` `count`	—	`Prod.mk_right_injective` `Finset.singleton_product` `Finset.ext`
`toEnumFinset_mono` 📖	mathematical	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Finset` `Finset.instHasSubset` `toEnumFinset`	—	`lt_of_le_of_lt'` `le_iff_count`
`toEnumFinset_subset_iff` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `toEnumFinset` `Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`map_toEnumFinset_fst` `map_fst_le_of_subset_toEnumFinset` `toEnumFinset_mono`

Multiset.instCoeSortMultisetType

Definitions

Name	Category	Theorems
`instCoeOutToType` 📖	CompOp	—

---

← Back to Index