Theorems · Theorem · logic and foundations

Set.Finite.encard_biUnion

∀ {α : Type u_1} {ι : Type u_2} {t : Set ι},
  t.Finite → ∀ {s : ι → Set α}, t.PairwiseDisjoint s → (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Defined in

Mathlib.Data.Set.Card.Arithmetic

Cited by

1 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound