coe_count

Mathlib.Data.Multiset.Count

URI: https://scilib.ai/kg/mathlib#Multiset.coe_count

← MathLib Explorer

English

For any a and list l, count a (ofList l) equals l.count a.

Русский

Для любого элемента a и списка l, count a (ofList l) равно l.count a.

LaTeX

$$$\operatorname{count}(a, \operatorname{ofList}(l)) = l.count(a)$$$

Lean4

@[simp]
theorem coe_count (a : α) (l : List α) : count a (ofList l) = l.count a :=
  by
  simp_rw [count, List.count, coe_countP (a = ·) l, @eq_comm _ a]
  rfl

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

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

Разделы

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

Аффилиация

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