card_disjiUnion — Mathlib

English

If s is partitioned into disjoint parts s₁, s₂ via disjiUnion, then |s.disjiUnion t h| = ∑ a ∈ s |t a|.

Русский

Если s разложено на непересекающиеся части s₁, s₂ через disjiUnion, то |s.disjiUnion t h| = ∑ a ∈ s |t a|.

LaTeX

$$$$\\#(s.disjiUnion t h) = \\sum a \\in s, \\#(t a)$$$$

Lean4

@[simp]
theorem card_disjiUnion (s : Finset ι) (t : ι → Finset M) (h) : #(s.disjiUnion t h) = ∑ a ∈ s, #(t a) :=
  Multiset.card_bind _ _

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