Theorem: ENat.tsum_iUnion_le (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
inst✝ : Fintype ι
f : α → ℕ∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑ i : ι, ∑' (x : ↑(t i)), f ↑x
Tactic:
rw [← tsum_fintype]
State after:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
inst✝ : Fintype ι
f : α → ℕ∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
inst✝ : Fintype ι
f : α → ℕ∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x
Tactic:
exact ENat.tsum_iUnion_le_tsum f t
State after:
no goals