duplicate_iff_two_le_count — Mathlib

English

With decidable equality, x is duplicated in l iff count x l ≥ 2.

Русский

При разрешимости равенства x дублируется в l тогда, когда количество x в l не менее двух.

LaTeX

$$$[DecidableEq\ \alpha]\ x \in+ l \iff 2 \le count\ x\ l$$$

Lean4

theorem duplicate_iff_two_le_count [DecidableEq α] : x ∈+ l ↔ 2 ≤ count x l := by
  simp [replicate_succ, duplicate_iff_sublist, ← replicate_sublist_iff]

Похожие утверждения