intro i hi
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
⊢ ∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
i : ι
hi : i ∈ J
⊢ LowerSemicontinuousWithinAt (f i) s a