Theorems · Theorem · combinatorics

Setoid.IsPartition.ncard_eq_finsum

∀ {α : Type u_1} {P : Set (Set α)},
  Setoid.IsPartition P →
    ∀ (s : Set α), autoParam s.Finite Setoid.IsPartition.ncard_eq_finsum._auto_1 → s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard

Given a partition of the ambient type, the cardinal of a finite set is the finsum of the cardinalities of its traces on the parts of the partition

Defined in

Mathlib.Data.Setoid.Partition.Card

Cited by

2 results in Mathlib

Foundations

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