powersetCard_map — Mathlib

English

Applying a function f to the elements of s commutes with taking powersetCard: powersetCard n (s.map f) = (powersetCard n s).map (map f).

Русский

Применение функции f к элементам s commuting с образованием powersetCard: powersetCard n (s.map f) = (powersetCard n s).map (map f).

LaTeX

$$$\mathrm{powersetCard}(n, s.map f) = (\mathrm{powersetCard}(n, s)).map (\mathrm{map} f)$$$

Lean4

theorem powersetCard_map {β : Type*} (f : α → β) (n : ℕ) (s : Multiset α) :
    powersetCard n (s.map f) = (powersetCard n s).map (map f) := by
  induction s using Multiset.induction generalizing n with
  | empty => cases n <;> simp [powersetCard_zero_left]
  | cons t s ih => cases n <;> simp [ih]

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