Dedup

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

Statistics

Metric	Count
Definitions	0
Theorems `dedup_append`, `union_eq`, `dedup`, `dedup`, `dedup_append_right`, `count_dedup`, `dedup_append`, `dedup_cons`, `dedup_cons'`, `dedup_cons_of_mem`, `dedup_cons_of_mem'`, `dedup_cons_of_notMem`, `dedup_cons_of_notMem'`, `dedup_eq_cons`, `dedup_eq_nil`, `dedup_eq_self`, `dedup_idem`, `dedup_map_of_injective`, `dedup_nil`, `dedup_sublist`, `dedup_subset`, `headI_dedup`, `mem_dedup`, `nodup_dedup`, `replicate_dedup`, `subset_dedup`, `tail_dedup`	27
Total	27

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_dedup` 📖	mathematical	—	`dedup`	—	`nodup_dedup`
`dedup_append` 📖	mathematical	—	`dedup`	—	`dedup_cons_of_mem'` `dedup_cons_of_notMem'`
`dedup_cons` 📖	mathematical	—	`dedup`	—	`dedup_cons'`
`dedup_cons'` 📖	mathematical	—	`dedup`	—	`dedup_cons_of_notMem'` `dedup_cons_of_mem'`
`dedup_cons_of_mem` 📖	mathematical	—	`dedup`	—	`dedup_cons_of_mem'` `mem_dedup`
`dedup_cons_of_mem'` 📖	—	`dedup`	—	—	—
`dedup_cons_of_notMem` 📖	mathematical	—	`dedup`	—	`dedup_cons_of_notMem'` `mem_dedup`
`dedup_cons_of_notMem'` 📖	—	`dedup`	—	—	—
`dedup_eq_cons` 📖	mathematical	—	`dedup`	—	`mem_dedup` `nodup_iff_count_le_one` `nodup_dedup` `cons_head!_tail`
`dedup_eq_nil` 📖	mathematical	—	`dedup`	—	`dedup_cons_of_mem` `dedup_cons_of_notMem`
`dedup_eq_self` 📖	mathematical	—	`dedup`	—	—
`dedup_idem` 📖	mathematical	—	`dedup`	—	—
`dedup_map_of_injective` 📖	mathematical	—	`dedup`	—	`dedup_cons_of_mem` `dedup_cons_of_notMem` `Iff.not` `mem_map_of_injective`
`dedup_nil` 📖	mathematical	—	`dedup`	—	—
`dedup_sublist` 📖	mathematical	—	`dedup`	—	—
`dedup_subset` 📖	mathematical	—	`dedup`	—	—
`headI_dedup` 📖	mathematical	—	`headI` `dedup`	—	`dedup_cons_of_mem` `dedup_cons_of_notMem`
`mem_dedup` 📖	mathematical	—	`dedup`	—	`not_and_or`
`nodup_dedup` 📖	mathematical	—	`dedup`	—	—
`replicate_dedup` 📖	mathematical	—	`dedup`	—	`dedup_cons_of_mem`
`subset_dedup` 📖	mathematical	—	`dedup`	—	`mem_dedup`
`tail_dedup` 📖	mathematical	—	`dedup` `headI`	—	`dedup_cons_of_mem` `dedup_cons_of_notMem`

List.Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedup_append` 📖	mathematical	—	`List.dedup`	—	`List.dedup_append` `union_eq` `List.mem_dedup`
`union_eq` 📖	mathematical	—	`List.dedup`	—	`List.dedup_cons_of_mem` `List.mem_union_left` `List.dedup_cons_of_notMem`

List.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedup` 📖	mathematical	—	`List.dedup`	—	`List.dedup_eq_self`

List.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedup` 📖	mathematical	—	`List.dedup`	—	`List.count_eq_one_of_mem`

List.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedup_append_right` 📖	mathematical	—	`List.dedup`	—	`List.dedup_append` `union_eq_right` `List.subset_dedup`

---

← Back to Index