card_pmap

Mathlib.Data.Multiset.Defs

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

English

The cardinality is preserved under pmap: card(pmap f s H) = card(s).

Русский

Кардинал сохраняется под pmap: card(pmap f s H) = card(s).

LaTeX

$$$\\operatorname{card}(\\operatorname{pmap}f\\ s\\ H)=\\operatorname{card}(s).$$$

Lean4

@[simp]
theorem card_pmap {p : α → Prop} (f : ∀ a, p a → β) (s H) : card (pmap f s H) = card s :=
  Quot.inductionOn s (fun _l _H => length_pmap) H

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

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

Разделы

Аффилиация

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