intro _
case refine'_1
β : 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
⊢ (∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ ∅, f i x) s a
case refine'_1
β : 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
hf✝ : ∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s a
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ ∅, f i x) s a