count_eq_one_of_mem

Mathlib.Data.List.Nodup

URI: https://scilib.ai/kg/mathlib#List.count_eq_one_of_mem

← MathLib Explorer

English

If l is nodup and a ∈ l, then the count of a in l is exactly 1.

Русский

Если l нодуп и a ∈ l, то количество a в l равно 1.

LaTeX

$$[DecidableEq α] {a} {l} (d : Nodup l) (h : a ∈ l) : count a l = 1$$

Lean4

@[simp]
theorem count_eq_one_of_mem [DecidableEq α] {a : α} {l : List α} (d : Nodup l) (h : a ∈ l) : count a l = 1 :=
  _root_.le_antisymm (nodup_iff_count_le_one.1 d a) (Nat.succ_le_of_lt (count_pos_iff.2 h))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru