encard of Sigma type

Stream: Is there code for X?

[Gareth Ma]

Hi, does the following exist in Mathlib?

example {ι α : Type*} {s : ι → Set α} :
    (Set.univ : Set (Σ i, s i)).encard = ∑' i, (Set.univ : Set (s i)).encard := by
  sorry

And if not, how should I prove it? I specifically want to manipulate statements about encard, but it seems a ton of API is missing. Cardinal seems easier to work with but I can't find any way to bridge Cardinal.sum with tsum

[Edward van de Meent]

it should be doable to do this on a by-case basis of if the set is infinite or not, as in the infinite case, showing that both sides are top should be easy, and in the other case, you can coerce to using Finsets and actual Finset.sum.

[Edward van de Meent]

fwiw i don't think this is in mathlib, but it should be. For reference of how you might prove such a thing, look at docs#ENNReal.tsum_set_one_eq , although i imagine the Sigma might throw a wrench here or there

[Gareth Ma]

Hmm I am struggling quite a bit, I will leave it for now

[Gareth Ma]

example {ι : Type*} {α : ι → Type*} [Fintype (Σ i : ι, α i)] : ∀ i, Fintype (α i) := by
  exact?

example {ι α : Type*} {s : ι → Set α} :
    (Set.univ : Set (Σ i, s i)).encard = ∑' i, (Set.univ : Set (s i)).encard := by
  simp_rw [Set.encard_univ_coe]
  classical
  by_cases h : Finite (Set.univ : Set (Σ i, s i))
  · sorry
  · convert refl ⊤
    · simp
      rwa [Set.Infinite, Set.Finite]
    · sorry