case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I : Finset ι
h✝ : ∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)
h : ∀ (i : ι), i ∈ ∅ → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (∑ i in ∅, κs i)

case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
⊢ IsSFiniteKernel (∑ i in insert i I, κs i)
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I : Finset ι
h : ∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (∑ i in I, κs i)
induction' I using Finset.induction with i I hi_nmem_I h_ind h
case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I : Finset ι
h✝ : ∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)
h : ∀ (i : ι), i ∈ ∅ → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel 0
case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I : Finset ι
h✝ : ∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)
h : ∀ (i : ι), i ∈ ∅ → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (∑ i in ∅, κs i)
rw [Finset.sum_empty]
no goals
case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I : Finset ι
h✝ : ∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)
h : ∀ (i : ι), i ∈ ∅ → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel 0
infer_instance
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
⊢ IsSFiniteKernel (κs i + ∑ x in I, κs x)
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
⊢ IsSFiniteKernel (∑ i in insert i I, κs i)
rw [Finset.sum_insert hi_nmem_I]
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
this : IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (κs i + ∑ x in I, κs x)
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
⊢ IsSFiniteKernel (κs i + ∑ x in I, κs x)
haveI : IsSFiniteKernel (κs i) := h i (Finset.mem_insert_self _ _)
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
this✝ : IsSFiniteKernel (κs i)
this : IsSFiniteKernel (∑ x in I, κs x)
⊢ IsSFiniteKernel (κs i + ∑ x in I, κs x)
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
this : IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (κs i + ∑ x in I, κs x)
have : IsSFiniteKernel (∑ x : ι in I, κs x) :=
  h_ind fun i hiI => h i (Finset.mem_insert_of_mem hiI)
no goals
case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
κs : ι → { x // x ∈ kernel α β }
I✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ I✝ → IsSFiniteKernel (κs i)
i : ι
I : Finset ι
hi_nmem_I : ¬i ∈ I
h_ind : (∀ (i : ι), i ∈ I → IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i in I, κs i)
h : ∀ (i_1 : ι), i_1 ∈ insert i I → IsSFiniteKernel (κs i_1)
this✝ : IsSFiniteKernel (κs i)
this : IsSFiniteKernel (∑ x in I, κs x)
⊢ IsSFiniteKernel (κs i + ∑ x in I, κs x)
exact IsSFiniteKernel.add _ _