case empty
α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.104654
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha✝ : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x
ha : ∀ (i : ι), i ∈ ∅ → LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in ∅, f i z) s x

case insert
α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.104654
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : Finset ι
ha✝ : ∀ (i : ι), i ∈ a✝ → LowerSemicontinuousWithinAt (f i) s x
i : ι
a : Finset ι
ia : ¬i ∈ a
IH :
  (∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x) →
    LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) s x
ha : ∀ (i_1 : ι), i_1 ∈ insert i a → LowerSemicontinuousWithinAt (f i_1) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in insert i a, f i z) s x
α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.104654
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) s x
induction' a using Finset.induction_on with i a ia IH
no goals
case empty
α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.104654
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha✝ : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x
ha : ∀ (i : ι), i ∈ ∅ → LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in ∅, f i z) s x
exact lowerSemicontinuousWithinAt_const
case insert
α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.104654
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : Finset ι
ha✝ : ∀ (i : ι), i ∈ a✝ → LowerSemicontinuousWithinAt (f i) s x
i : ι
a : Finset ι
ia : ¬i ∈ a
IH :
  (∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x) →
    LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) s x
ha : ∀ (i_1 : ι), i_1 ∈ insert i a → LowerSemicontinuousWithinAt (f i_1) s x
⊢ LowerSemicontinuousWithinAt (fun z => f i z + ∑ i in a, f i z) s x
case insert
α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.104654
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : Finset ι
ha✝ : ∀ (i : ι), i ∈ a✝ → LowerSemicontinuousWithinAt (f i) s x
i : ι
a : Finset ι
ia : ¬i ∈ a
IH :
  (∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x) →
    LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) s x
ha : ∀ (i_1 : ι), i_1 ∈ insert i a → LowerSemicontinuousWithinAt (f i_1) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in insert i a, f i z) s x
simp only [ia, Finset.sum_insert, not_false_iff]
no goals
case insert
α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.104654
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : Finset ι
ha✝ : ∀ (i : ι), i ∈ a✝ → LowerSemicontinuousWithinAt (f i) s x
i : ι
a : Finset ι
ia : ¬i ∈ a
IH :
  (∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) s x) →
    LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) s x
ha : ∀ (i_1 : ι), i_1 ∈ insert i a → LowerSemicontinuousWithinAt (f i_1) s x
⊢ LowerSemicontinuousWithinAt (fun z => f i z + ∑ i in a, f i z) s x
exact
  LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self i a))
    (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))