Theorems · Theorem · combinatorics

List.duplicate_iff_exists_distinct_get

∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l ↔ ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m

An element x : α of l : List α is a duplicate iff it can be found at two distinct indices n m : ℕ inside the list l.

Defined in

Mathlib.Data.List.NodupEquivFin

Cited by

0 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound