English
Let l be a finite list in α and a ∈ α. The set of elements of l is the singleton {a} if and only if l is a replication of a: l = replicate n a for some n > 0.
Русский
Пусть l — конечный список элементов типа α. Множество элементов списка l равно {a} тогда и только тогда, когда l состоит из повторений элемента a, то есть l = replicate n a с n > 0.
LaTeX
$$$\{ x \mid x \in l \} = \{ a \} \iff \exists n \in \mathbb{N}, n > 0 \land l = \operatorname{replicate}(n,a)$$$
Lean4
theorem setOf_mem_list_eq_replicate {l : List α} {a : α} : {x | x ∈ l} = { a } ↔ ∃ n > 0, l = List.replicate n a := by
simpa +contextual [Set.ext_iff, iff_iff_implies_and_implies, forall_and, List.eq_replicate_iff,
List.length_pos_iff_exists_mem] using ⟨fun _ _ ↦ ⟨_, ‹_›⟩, fun x hx h ↦ h _ hx ▸ hx⟩
