Documentation Verification Report

Duplicate

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

Statistics

Metric	Count
Definitions `Duplicate`, `decidableDuplicate`	2
Theorems `duplicate_cons`, `elim_nil`, `elim_singleton`, `mem`, `mem_cons_self`, `mono_sublist`, `ne_nil`, `ne_singleton`, `not_nodup`, `of_duplicate_cons`, `duplicate_cons_self`, `duplicate_cons_iff`, `duplicate_cons_iff_of_ne`, `duplicate_cons_self_iff`, `duplicate_iff_sublist`, `duplicate_iff_two_le_count`, `exists_duplicate_iff_not_nodup`, `nodup_iff_forall_not_duplicate`, `not_duplicate_nil`, `not_duplicate_singleton`	20
Total	22

List

Definitions

Name	Category	Theorems
`Duplicate` 📖	CompData	11 math math: `duplicate_iff_exists_distinct_get`, `nodup_iff_forall_not_duplicate`, `Mem.duplicate_cons_self`, `duplicate_cons_iff_of_ne`, `not_duplicate_singleton`, `not_duplicate_nil`, `duplicate_cons_iff`, `duplicate_iff_sublist`, `duplicate_cons_self_iff`, `exists_duplicate_iff_not_nodup`, `duplicate_iff_two_le_count`
`decidableDuplicate` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`duplicate_cons_iff` 📖	mathematical	—	`Duplicate`	—	—
`duplicate_cons_iff_of_ne` 📖	mathematical	—	`Duplicate`	—	—
`duplicate_cons_self_iff` 📖	mathematical	—	`Duplicate`	—	`Duplicate.mem_cons_self` `Mem.duplicate_cons_self`
`duplicate_iff_sublist` 📖	mathematical	—	`Duplicate`	—	`duplicate_cons_iff_of_ne` `sublist_cons_of_sublist`
`duplicate_iff_two_le_count` 📖	mathematical	—	`Duplicate`	—	—
`exists_duplicate_iff_not_nodup` 📖	mathematical	—	`Duplicate`	—	—
`nodup_iff_forall_not_duplicate` 📖	mathematical	—	`Duplicate`	—	—
`not_duplicate_nil` 📖	mathematical	—	`Duplicate`	—	`Duplicate.ne_nil`
`not_duplicate_singleton` 📖	mathematical	—	`Duplicate`	—	`Duplicate.ne_singleton`

List.Duplicate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`duplicate_cons` 📖	—	`List.Duplicate`	—	—	—
`elim_nil` 📖	—	`List.Duplicate`	—	—	`List.not_duplicate_nil`
`elim_singleton` 📖	—	`List.Duplicate`	—	—	`List.not_duplicate_singleton`
`mem` 📖	—	`List.Duplicate`	—	—	—
`mem_cons_self` 📖	—	`List.Duplicate`	—	—	`mem`
`mono_sublist` 📖	—	`List.Duplicate`	—	—	`duplicate_cons` `List.duplicate_cons_iff`
`ne_nil` 📖	—	`List.Duplicate`	—	—	`mem`
`ne_singleton` 📖	—	`List.Duplicate`	—	—	`mem`
`not_nodup` 📖	—	`List.Duplicate`	—	—	`List.nodup_iff_forall_not_duplicate`
`of_duplicate_cons` 📖	—	`List.Duplicate`	—	—	—

List.Mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`duplicate_cons_self` 📖	mathematical	—	`List.Duplicate`	—	—

---

← Back to Index