count_map_of_injective — Mathlib

English

If f is injective, then for every x, the number of occurrences of f(x) in the image map f l equals the number of occurrences of x in l.

Русский

Если отображение f инъективно, то для каждого x число вхождений f(x) в отображённом списке map f l равно числу вхождений x в l.

LaTeX

$$$\\forall x,\\ count (f x) (map f\\ l) = count\\ x\\ l \\quad \\text{(assuming injective } f\\text{)}$$$

Lean4

@[simp]
theorem count_map_of_injective [DecidableEq β] (l : List α) (f : α → β) (hf : Function.Injective f) (x : α) :
    count (f x) (map f l) = count x l := by
  simp only [count, countP_map]
  unfold Function.comp
  simp only [hf.beq_eq]

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