case inl
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Fintype ι
⊢ IsSFiniteKernel (kernel.sum κs)

case inr
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Infinite ι
⊢ IsSFiniteKernel (kernel.sum κs)
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
⊢ IsSFiniteKernel (kernel.sum κs)
cases fintypeOrInfinite ι
case inr.intro
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝¹ : Infinite ι
val✝ : Denumerable ι
⊢ IsSFiniteKernel (kernel.sum κs)
case inr
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Infinite ι
⊢ IsSFiniteKernel (kernel.sum κs)
cases nonempty_denumerable ι
no goals
case inr.intro
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝¹ : Infinite ι
val✝ : Denumerable ι
⊢ IsSFiniteKernel (kernel.sum κs)
exact isSFiniteKernel_sum_of_denumerable hκs
case inl
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Fintype ι
⊢ IsSFiniteKernel (∑ i : ι, κs i)
case inl
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Fintype ι
⊢ IsSFiniteKernel (kernel.sum κs)
rw [sum_fintype]
no goals
case inl
α : Type u_2
β : Type u_3
ι : Type u_1
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
inst✝ : Countable ι
κs : ι → { x // x ∈ kernel α β }
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Fintype ι
⊢ IsSFiniteKernel (∑ i : ι, κs i)
exact IsSFiniteKernel.finset_sum Finset.univ fun i _ => hκs i