Bind

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

Statistics

Metric	Count
Definitions `bind`, `instSProd`, `join`, `product`, `sigma`	5
Theorems `product`, `sigma`, `add_bind`, `add_product`, `add_sigma`, `attach_bind_coe`, `bind_add`, `bind_assoc`, `bind_bind`, `bind_congr`, `bind_cons`, `bind_filter`, `bind_filterMap`, `bind_hcongr`, `bind_map`, `bind_map_comm`, `bind_singleton`, `bind_zero`, `card_bind`, `card_join`, `card_product`, `card_sigma`, `coe_bind`, `coe_join`, `coe_product`, `coe_sigma`, `cons_bind`, `cons_product`, `cons_sigma`, `count_bind`, `count_sum`, `dedup_bind_dedup`, `filterMap_bind`, `filterMap_eq_bind`, `filterMap_join`, `filter_bind`, `filter_eq_bind`, `filter_join`, `fold_bind`, `join_add`, `join_cons`, `join_zero`, `le_bind`, `map_bind`, `map_join`, `map_swap_product`, `mem_bind`, `mem_join`, `mem_product`, `mem_sigma`, `nodup_bind`, `prod_bind`, `prod_join`, `prod_map_product_eq_prod_prod`, `product_add`, `product_cons`, `product_singleton`, `product_zero`, `rel_bind`, `rel_join`, `sigma_add`, `sigma_singleton`, `singleton_bind`, `singleton_join`, `sum_bind`, `sum_join`, `zero_bind`, `zero_product`, `zero_sigma`	69
Total	74

Multiset

Definitions

Name	Category	Theorems
`bind` 📖	CompOp	44 math math: `pi_cons`, `dedup_bind_dedup`, `bind_hcongr`, `prod_bind`, `coe_bind`, `bind_bind`, `Finset.biUnion_val`, `bind_filterMap`, `bind_zero`, `map_bind`, `bind_filter`, `bind_add`, `bind_singleton`, `nodup_bind`, `singleton_bind`, `bind_map_comm`, `filterMap_eq_bind`, `sections_cons`, `count_bind`, `add_bind`, `Polynomial.roots_prod`, `sum_bind`, `fold_bind`, `Polynomial.roots_list_prod`, `filter_bind`, `mem_bind`, `bind_assoc`, `bind_cons`, `filterMap_bind`, `bind_def`, `sections_add`, `attach_bind_coe`, `filter_eq_bind`, `bind_congr`, `Polynomial.roots_multiset_prod`, `zero_bind`, `bind_map`, `cons_bind`, `bind_powerset_len`, `rel_bind`, `card_bind`, `Finset.disjiUnion_val`, `le_bind`, `Finset.bind_toFinset`
`instSProd` 📖	CompOp	18 math math: `product_cons`, `zero_product`, `coe_product`, `product_singleton`, `Polynomial.map_sub_roots_sprod_eq_prod_map_eval`, `sum_smul_sum`, `product_zero`, `Polynomial.map_sub_sprod_roots_eq_prod_map_eval`, `prod_map_product_eq_prod_prod`, `Finset.product_val`, `card_product`, `cons_product`, `Polynomial.resultant_eq_prod_roots_sub`, `product_add`, `add_product`, `map_swap_product`, `Nodup.product`, `mem_product`
`join` 📖	CompOp	13 math math: `join_zero`, `prod_join`, `singleton_join`, `join_add`, `rel_join`, `filter_join`, `join_cons`, `card_join`, `mem_join`, `sum_join`, `map_join`, `coe_join`, `filterMap_join`
`product` 📖	CompOp	—
`sigma` 📖	CompOp	9 math math: `sigma_singleton`, `mem_sigma`, `Nodup.sigma`, `coe_sigma`, `add_sigma`, `cons_sigma`, `zero_sigma`, `card_sigma`, `sigma_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_bind` 📖	mathematical	—	`bind` `Multiset` `instAdd`	—	`map_add` `join_add`
`add_product` 📖	mathematical	—	`SProd.sprod` `Multiset` `instSProd` `instAdd`	—	`add_bind`
`add_sigma` 📖	mathematical	—	`sigma` `Multiset` `instAdd`	—	`add_bind`
`attach_bind_coe` 📖	mathematical	—	`bind` `Multiset` `instMembership` `attach`	—	`attach_map_val'`
`bind_add` 📖	mathematical	—	`bind` `Multiset` `instAdd`	—	`sum_map_add`
`bind_assoc` 📖	mathematical	—	`bind`	—	`induction_on` `cons_bind` `add_bind`
`bind_bind` 📖	mathematical	—	`bind`	—	`induction_on` `bind_zero` `cons_bind` `bind_add`
`bind_congr` 📖	mathematical	—	`bind`	—	`map_congr`
`bind_cons` 📖	mathematical	—	`bind` `cons` `Multiset` `instAdd` `map`	—	`induction_on` `add_zero` `add_comm` `cons_bind` `add_left_comm` `cons_add` `add_cons` `map_cons` `add_assoc`
`bind_filter` 📖	mathematical	—	`bind` `filter` `Multiset` `instZero`	—	`filter_eq_bind` `bind_assoc` `bind_congr` `singleton_bind`
`bind_filterMap` 📖	mathematical	—	`bind` `filterMap` `Multiset` `instZero`	—	`filterMap_eq_bind` `bind_assoc` `bind_congr` `singleton_bind`
`bind_hcongr` 📖	mathematical	`Multiset`	`bind`	—	`bind_congr`
`bind_map` 📖	mathematical	—	`bind` `map`	—	`induction_on` `map_cons` `cons_bind`
`bind_map_comm` 📖	mathematical	—	`bind` `map`	—	`induction_on` `bind_zero` `cons_bind` `map_cons` `bind_cons`
`bind_singleton` 📖	mathematical	—	`bind` `Multiset` `instSingleton` `map`	—	`induction_on` `zero_bind` `map_zero` `cons_bind` `map_cons`
`bind_zero` 📖	mathematical	—	`bind` `Multiset` `instZero`	—	`map_const'` `sum_replicate` `nsmul_zero`
`card_bind` 📖	mathematical	—	`card` `bind` `sum` `Nat.instAddCommMonoid` `map` `Multiset`	—	`card_join` `map_map` `map_congr`
`card_join` 📖	mathematical	—	`card` `join` `sum` `Nat.instAddCommMonoid` `map` `Multiset`	—	`induction_on` `join_cons` `card_add` `map_cons` `sum_cons`
`card_product` 📖	mathematical	—	`card` `SProd.sprod` `Multiset` `instSProd`	—	`card_bind` `map_congr` `card_map` `map_const'` `sum_replicate`
`card_sigma` 📖	mathematical	—	`card` `sigma` `sum` `Nat.instAddCommMonoid` `map`	—	`card_bind` `map_congr` `card_map`
`coe_bind` 📖	mathematical	—	`bind` `ofList`	—	`coe_join`
`coe_join` 📖	mathematical	—	`join` `ofList` `Multiset`	—	—
`coe_product` 📖	mathematical	—	`SProd.sprod` `Multiset` `instSProd` `ofList` `List.instSProd`	—	`product.eq_1` `coe_bind`
`coe_sigma` 📖	mathematical	—	`sigma` `ofList`	—	`sigma.eq_1` `coe_bind`
`cons_bind` 📖	mathematical	—	`bind` `cons` `Multiset` `instAdd`	—	`map_cons` `join_cons`
`cons_product` 📖	mathematical	—	`SProd.sprod` `Multiset` `instSProd` `cons` `instAdd` `map`	—	`cons_bind`
`cons_sigma` 📖	mathematical	—	`sigma` `cons` `Multiset` `instAdd` `map`	—	`cons_bind`
`count_bind` 📖	mathematical	—	`count` `bind` `sum` `Nat.instAddCommMonoid` `map`	—	`count_sum`
`count_sum` 📖	mathematical	—	`count` `sum` `Multiset` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `map` `Nat.instAddCommMonoid`	—	`induction_on` `count_eq_zero_of_notMem` `count.congr_simp` `map_cons` `sum_cons` `count_add`
`dedup_bind_dedup` 📖	mathematical	—	`dedup` `bind`	—	`ext'` `count_dedup`
`filterMap_bind` 📖	mathematical	—	`filterMap` `bind`	—	`filterMap_join` `map_map` `map_congr`
`filterMap_eq_bind` 📖	mathematical	—	`filterMap` `bind` `Multiset` `instSingleton` `instZero`	—	`induction` `filterMap_cons` `cons_bind`
`filterMap_join` 📖	mathematical	—	`filterMap` `join` `map` `Multiset`	—	`induction` `join_cons` `filterMap_add` `map_cons`
`filter_bind` 📖	mathematical	—	`filter` `bind`	—	`filter_join` `map_map` `map_congr`
`filter_eq_bind` 📖	mathematical	—	`filter` `bind` `Multiset` `instSingleton` `instZero`	—	`induction` `filter_cons` `cons_bind`
`filter_join` 📖	mathematical	—	`filter` `join` `map` `Multiset`	—	`induction` `filter.congr_simp` `join_cons` `filter_add` `map_cons`
`fold_bind` 📖	mathematical	—	`fold` `map` `bind`	—	`induction_on` `zero_bind` `map_zero` `fold_zero` `cons_bind` `map_cons` `fold_cons_left` `fold_add`
`join_add` 📖	mathematical	—	`join` `Multiset` `instAdd`	—	`sum_add`
`join_cons` 📖	mathematical	—	`join` `cons` `Multiset` `instAdd`	—	`sum_cons`
`join_zero` 📖	mathematical	—	`join` `Multiset` `instZero`	—	—
`le_bind` 📖	mathematical	`Multiset` `instMembership`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `bind`	—	`le_iff_count` `exists_cons_of_mem` `mem_map_of_mem` `count_bind` `sum_cons`
`map_bind` 📖	mathematical	—	`map` `bind`	—	`map_join` `map_map` `map_congr`
`map_join` 📖	mathematical	—	`map` `join` `Multiset`	—	`induction` `map_congr` `join_cons` `map_add` `map_cons`
`map_swap_product` 📖	mathematical	—	`map` `SProd.sprod` `Multiset` `instSProd`	—	`induction` `product_zero` `map_congr` `cons_product` `map_add` `map_map` `product_cons`
`mem_bind` 📖	mathematical	—	`Multiset` `instMembership` `bind`	—	—
`mem_join` 📖	mathematical	—	`Multiset` `instMembership` `join`	—	`induction_on` `join_cons`
`mem_product` 📖	mathematical	—	`Multiset` `instMembership` `SProd.sprod` `instSProd`	—	—
`mem_sigma` 📖	mathematical	—	`Multiset` `instMembership` `sigma`	—	—
`nodup_bind` 📖	mathematical	—	`Nodup` `bind` `Pairwise` `Function.onFun` `Multiset` `Disjoint` `instPartialOrder` `instOrderBot`	—	`Quot.induction_on` `List.Disjoint.symm` `coe_bind` `pairwise_coe_iff_pairwise`
`prod_bind` 📖	mathematical	—	`prod` `bind` `map`	—	`prod_join` `map_map` `map_congr`
`prod_join` 📖	mathematical	—	`prod` `join` `map` `Multiset`	—	`induction` `join_cons` `prod_add` `map_cons` `prod_cons`
`prod_map_product_eq_prod_prod` 📖	mathematical	—	`prod` `map` `SProd.sprod` `Multiset` `instSProd`	—	`induction` `map_congr` `cons_product` `map_add` `map_map` `prod_add` `map_cons` `prod_cons`
`product_add` 📖	mathematical	—	`SProd.sprod` `Multiset` `instSProd` `instAdd`	—	`induction_on` `cons_product` `map_add` `add_assoc` `add_left_comm`
`product_cons` 📖	mathematical	—	`SProd.sprod` `Multiset` `instSProd` `cons` `instAdd` `map`	—	`map_cons` `bind_cons`
`product_singleton` 📖	mathematical	—	`SProd.sprod` `Multiset` `instSProd` `instSingleton`	—	`bind_singleton`
`product_zero` 📖	mathematical	—	`SProd.sprod` `Multiset` `instSProd` `instZero`	—	`bind_zero`
`rel_bind` 📖	mathematical	`Relator.LiftFun` `Multiset` `Rel`	`bind`	—	`rel_join` `rel_map` `Rel.mono`
`rel_join` 📖	mathematical	`Rel` `Multiset`	`join`	—	`join_cons` `Rel.add`
`sigma_add` 📖	mathematical	—	`sigma` `Multiset` `instAdd`	—	`induction_on` `cons_sigma` `map_add` `add_comm` `add_assoc` `add_left_comm`
`sigma_singleton` 📖	mathematical	—	`sigma` `Multiset` `instSingleton`	—	—
`singleton_bind` 📖	mathematical	—	`bind` `Multiset` `instSingleton`	—	`singleton_join`
`singleton_join` 📖	mathematical	—	`join` `Multiset` `instSingleton`	—	`sum_singleton`
`sum_bind` 📖	mathematical	—	`sum` `bind` `map`	—	`sum_join` `map_map` `map_congr`
`sum_join` 📖	mathematical	—	`sum` `join` `map` `Multiset`	—	`induction` `join_cons` `sum_add` `map_cons` `sum_cons`
`zero_bind` 📖	mathematical	—	`bind` `Multiset` `instZero`	—	—
`zero_product` 📖	mathematical	—	`SProd.sprod` `Multiset` `instSProd` `instZero`	—	—
`zero_sigma` 📖	mathematical	—	`sigma` `Multiset` `instZero`	—	—

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`product` 📖	mathematical	`Multiset.Nodup`	`SProd.sprod` `Multiset` `Multiset.instSProd`	—	`Multiset.coe_product` `List.Nodup.product`
`sigma` 📖	mathematical	`Multiset.Nodup`	`Multiset.sigma`	—	`Quot.induction_on` `Multiset.coe_sigma` `List.Nodup.sigma`

---

← Back to Index