card_antidiagonal — Mathlib

English

The number of elements in the antidiagonal of a multiset s is 2 raised to the power of the number of elements of s.

Русский

Число элементов антидиагонали мультимножества s равно 2^{|s|}.

LaTeX

$$$\\operatorname{card}(\\operatorname{antidiagonal}(s)) = 2^{\\operatorname{card}(s)}$$$

Lean4

@[simp]
theorem card_antidiagonal (s : Multiset α) : card (antidiagonal s) = 2 ^ card s :=
  by
  have := card_powerset s
  rwa [← antidiagonal_map_fst, card_map] at this

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