Theorems · Inductive type · combinatorics
List.Duplicate
{α : Type u_1} → α → List α → PropProperty that an element x : α of l : List α can be found in the list more than once.
- Defined in
- Mathlib.Data.List.Duplicate
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by28
Results whose statement or proof uses this declaration.
- List.Duplicate.memstatement and proof · cited by 3
- List.nodup_iff_forall_not_duplicatestatement and proof · cited by 2
- List.Duplicate.casesOnstatement and proof · cited by 2
- List.duplicate_iff_two_le_countstatement · cited by 2
- List.exists_duplicate_iff_not_nodupstatement and proof · cited by 1
- List.not_duplicate_nilstatement and proof · cited by 1
- List.not_duplicate_singletonstatement and proof · cited by 1
- List.Duplicate.belowstatement · cited by 1
- List.Duplicate.duplicate_consstatement and proof · cited by 1
- List.Duplicate.mem_cons_selfstatement and proof · cited by 1
- List.Duplicate.ne_nilstatement and proof · cited by 1
- List.Duplicate.ne_singletonstatement and proof · cited by 1