card_map — Mathlib

English

Let f: α → β be a function and s a multiset of α. Then the multiset obtained by applying f to every element of s has the same cardinality as s.

Русский

Пусть f: α → β — функция, и s — мультимножество элементов α. Тогда мультимножество, полученное применением f к каждому элементу s, имеет ту же кардинальность, что и s.

LaTeX

$$$$ \\operatorname{card}(\\operatorname{map} f s) = \\operatorname{card} s $$$$

Lean4

@[simp]
theorem card_map (f : α → β) (s) : card (map f s) = card s :=
  Quot.inductionOn s fun _ => length_map _

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