map_val_val_powersetCard — Mathlib

English

Mapping the underlying values aligns powersetCard with the underlying multiset.

Русский

Переброс значений через отображение совпадает с powersetCard на базовом мультимножестве.

LaTeX

$$map Val (powersetCard i s).val = powersetCard i s.val$$

Lean4

@[simp]
theorem map_val_val_powersetCard (s : Finset α) (i : ℕ) : (s.powersetCard i).val.map Finset.val = s.1.powersetCard i :=
  by simp [Finset.powersetCard, map_pmap, pmap_eq_map, map_id']

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