card_filter_univ_eq_vector_get_eq_count

English

For a vector v and an element a, the number of indices i with v[i] = a equals the number of occurrences of a in v.

Русский

Для вектора v и элемента a число индексов i с v[i] = a равно числу вхождений a в v.

LaTeX

$$$ \\#\\{i\\mid v\\,\\text{get}\\, i = a\\} = \\text{List.count}(a, v) $$$

Lean4

theorem card_filter_univ_eq_vector_get_eq_count [DecidableEq α] (a : α) (v : List.Vector α n) :
    #{i | v.get i = a} = v.toList.count a := by
  induction v with
  | nil => simp
  | @cons n x xs hxs =>
    simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ, hxs,
      List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]

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