Dedup

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

Statistics

Metric	Count
Definitions `dedup`	1
Theorems `dedup_append_left`, `dedup_add`, `dedup`, `le_dedup_iff_le`, `dedup_add_left`, `dedup_add_right`, `coe_dedup`, `count_dedup`, `dedup_cons_of_mem`, `dedup_cons_of_notMem`, `dedup_eq_self`, `dedup_eq_zero`, `dedup_ext`, `dedup_idem`, `dedup_le`, `dedup_map_dedup_eq`, `dedup_map_of_injective`, `dedup_singleton`, `dedup_subset`, `dedup_subset'`, `dedup_zero`, `le_dedup`, `le_dedup_self`, `mem_dedup`, `nodup_dedup`, `subset_dedup`, `subset_dedup'`	27
Total	28

List.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedup_append_left` 📖	mathematical	—	`List.dedup`	—	`Multiset.coe_eq_coe` `Multiset.coe_dedup` `Multiset.coe_add` `Multiset.Subset.dedup_add_left`

Multiset

Definitions

Name	Category	Theorems
`dedup` 📖	CompOp	48 math math: `dedup_ext`, `dedup_cons`, `gcd_dedup`, `dedup_eq_zero`, `dedup_eq_self`, `dedup_bind_dedup`, `inf_dedup`, `dedup_card_eq_card_iff_nodup`, `Finset.biUnion_val`, `Finset.dedup_eq_self`, `le_dedup`, `dedup_add`, `dedup_nsmul`, `lcm_dedup`, `le_dedup_self`, `Disjoint.ndunion_eq`, `dedup_zero`, `mem_dedup`, `nodup_dedup`, `sup_dedup`, `dedup_map_of_injective`, `Finset.insert_val'`, `fold_dedup_idem`, `dedup_cons_of_notMem`, `count_dedup`, `dedup_le`, `dedup_idem`, `Finpartition.ofSetoid_parts_val`, `card_toFinset`, `Disjoint.dedup_add`, `coe_dedup`, `subset_dedup'`, `dedup_sym2`, `subset_dedup`, `Nodup.dedup`, `toFinset_dedup`, `dedup_cons_of_mem`, `Subset.dedup_add_right`, `dedup_subset'`, `Nodup.le_dedup_iff_le`, `Finset.image_val`, `le_smul_dedup`, `Subset.dedup_add_left`, `dedup_singleton`, `dedup_subset`, `dedup_map_dedup_eq`, `Finpartition.avoid_parts_val`, `toFinset_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_dedup` 📖	mathematical	—	`dedup` `ofList` `List.dedup`	—	—
`count_dedup` 📖	mathematical	—	`count` `dedup` `Multiset` `instMembership` `decidableMem`	—	`Quot.induction_on` `coe_count` `List.count_dedup`
`dedup_cons_of_mem` 📖	mathematical	`Multiset` `instMembership`	`dedup` `cons`	—	`Quot.induction_on` `List.dedup_cons_of_mem`
`dedup_cons_of_notMem` 📖	mathematical	`Multiset` `instMembership`	`dedup` `cons`	—	`Quot.induction_on` `List.dedup_cons_of_notMem`
`dedup_eq_self` 📖	mathematical	—	`dedup` `Nodup`	—	`nodup_dedup` `Quot.induction_on` `List.Nodup.dedup`
`dedup_eq_zero` 📖	mathematical	—	`dedup` `Multiset` `instZero`	—	`eq_zero_of_subset_zero` `subset_dedup` `dedup_zero`
`dedup_ext` 📖	mathematical	—	`dedup` `Multiset` `instMembership`	—	—
`dedup_idem` 📖	mathematical	—	`dedup`	—	`Quot.induction_on` `List.dedup_idem`
`dedup_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `dedup`	—	`Quot.induction_on` `List.dedup_sublist`
`dedup_map_dedup_eq` 📖	mathematical	—	`dedup` `map`	—	—
`dedup_map_of_injective` 📖	mathematical	—	`dedup` `map`	—	`Quot.induction_on` `List.dedup_map_of_injective`
`dedup_singleton` 📖	mathematical	—	`dedup` `Multiset` `instSingleton`	—	`Nodup.dedup` `nodup_singleton`
`dedup_subset` 📖	mathematical	—	`Multiset` `instHasSubset` `dedup`	—	`subset_of_le` `dedup_le`
`dedup_subset'` 📖	mathematical	—	`Multiset` `instHasSubset` `dedup`	—	`Subset.trans` `subset_dedup` `dedup_subset`
`dedup_zero` 📖	mathematical	—	`dedup` `Multiset` `instZero`	—	—
`le_dedup` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `dedup` `Nodup`	—	`le_trans` `dedup_le` `nodup_of_le` `nodup_dedup` `le_iff_subset` `Subset.trans` `subset_of_le` `subset_dedup`
`le_dedup_self` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `dedup` `Nodup`	—	`le_dedup` `le_rfl`
`mem_dedup` 📖	mathematical	—	`Multiset` `instMembership` `dedup`	—	`Quot.induction_on` `List.mem_dedup`
`nodup_dedup` 📖	mathematical	—	`Nodup` `dedup`	—	`Quot.induction_on` `List.nodup_dedup`
`subset_dedup` 📖	mathematical	—	`Multiset` `instHasSubset` `dedup`	—	`mem_dedup`
`subset_dedup'` 📖	mathematical	—	`Multiset` `instHasSubset` `dedup`	—	`Subset.trans` `dedup_subset` `subset_dedup`

Multiset.Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedup_add` 📖	mathematical	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot`	`Multiset.dedup` `Multiset.instAdd`	—	`Quot.induction_on₂` `List.Disjoint.dedup_append`

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedup` 📖	mathematical	`Multiset.Nodup`	`Multiset.dedup`	—	`Multiset.dedup_eq_self`
`le_dedup_iff_le` 📖	mathematical	`Multiset.Nodup`	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `Multiset.dedup`	—	—

Multiset.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedup_add_left` 📖	mathematical	`Multiset` `Multiset.instHasSubset`	`Multiset.dedup` `Multiset.instAdd`	—	`Multiset.add_comm` `dedup_add_right`
`dedup_add_right` 📖	mathematical	`Multiset` `Multiset.instHasSubset`	`Multiset.dedup` `Multiset.instAdd`	—	`Quot.induction_on₂` `List.Subset.dedup_append_right`

---

← Back to Index