Cardinality of the union of sets

Stream: general

[Teddy Baker]

I'm having trouble proving that the cardinality of a union of sets is equal to the sum of the cardinalities when the sets are disjoint. The only theorem that I see in mathlib for this is Finset.card_biUnion, which is for finsets. I can also prove by induction that the sum of the encards of the subsets is equal to the encard of the union, using Set.encard_union_eq, but the Disjoint property is unwieldy to prove by unfolding the definition, and generally this is a rather complicated approach. I have a few questions

1.) Is there an easier way to do all of this
2.) Should I first find the cardinalities of the subsets to show that they are finite, so that I can use Finset.card_biUnion

Here is an mwe,

import Mathlib

open Real
open Nat
open BigOperators

theorem encard_union
  (S : Set (ℕ × ℕ))
  (hS : S = {m | sorry}):
  S.encard = 50 := by

  let Sₙ : Fin 50 → Set (ℕ × ℕ) := sorry

  have union_eq : S = Set.iUnion Sₙ := by
      sorry

  have : S.encard = ∑ n in Finset.univ, (Sₙ n).encard := by

    have (i j : Fin 50) (h : i ≠ j): Disjoint (S i) (S j) := by
      sorry

    rw [union_eq]

    sorry

Any suggestions or help would be appreciated!

[Eric Wieser]

You're definitely in trouble with your statement, since it contains sorry! I think the statement that you want to prove is:

open scoped BigOperators

theorem Set.encard_iUnion_eq {ι α} (s : ι → Set α) (h : Pairwise (Disjoint on s)) :
  (⋃ i, s i).encard = ∑ᶠ i, (s i).encard := sorry

[Ruben Van de Velde]

How about this:

import Mathlib

open Real
open Nat
open BigOperators

theorem foo' (α ι : Type*) [Fintype ι] (f : ι → Set α) (s : Finset ι) (h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)) :
    Set.encard (⋃ i ∈ s, f i) = ∑ i in s, Set.encard (f i) := by
  induction s using Finset.cons_induction with
  | empty => simp
  | @cons i s hi ih =>
    simp
    rw [Set.encard_union_eq]
    · congr
      apply ih
      intros j hj k hk hjk
      apply h
      simp [hj]
      simp [hk]
      assumption
    · refine Set.disjoint_iUnion₂_right.mpr ?cons.a
      intros j hj
      apply h
      simp
      simp [hj]
      exact Ne.symm (ne_of_mem_of_not_mem hj hi)

theorem foo (α ι : Type*) [Fintype ι] (f : ι → Set α) (h : ∀ i j, i ≠ j → Disjoint (f i) (f j)) :
    Set.encard (⋃ i, f i) = ∑ i, Set.encard (f i) := by
  have := foo' α ι  f Finset.univ ?_
  simpa using this
  rintro i - j -
  apply h

[Teddy Baker]

Thanks!

[Eric Wieser]

(This sniped me into trying to go via the existing proof for Cardinal, which probably needs #9187)

[Peter Nelson]

Eric Wieser said:

You're definitely in trouble with your statement, since it contains sorry! I think the statement that you want to prove is:

open scoped BigOperators

theorem Set.encard_iUnion_eq {ι α} (s : ι → Set α) (h : Pairwise (Disjoint on s)) :
  (⋃ i, s i).encard = ∑ᶠ i, (s i).encard := sorry

This isn’t true - if all the sets in s are infinite and there are infinitely many of them, then the RHS is zero and the LHS is infinite.

The right generality here is tsum or cardinals.

[Eric Wieser]

Nice catch! I almost wrote tsum, but thought I would be safe...

[Peter Nelson]

I have a PR almost ready with that lemma and many others proved for tsum, but the annoying thing is that it doesn’t properly generalize the corresponding ENNReal statements.

[Eric Wieser]

#9187 (linked above) has the cardinal versions

[Peter Nelson]

Why doesn't that PR use PairwiseDisjoint?

[Eric Wieser]

The short answer is that I was matching the style of the existing lemmas there

[Eric Wieser]

A follow-up could indeed make that cleanup

[Eric Wieser]

Peter Nelson said:

Why doesn't that PR use PairwiseDisjoint?

#9236