dsimp at ht
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < (fun x => ⨆ i ∈ I, f i x) a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'
β : Type u_3
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f✝ : α → β
inst✝² : CompleteLinearOrder β
inst✝¹ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
inst✝ : TopologicalSpace ι
I : Set ι
ne_I : Set.Nonempty I
hI : IsCompact I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
hf' : UpperSemicontinuousOn (fun i => f i a) I
t : β
ht : t < ⨆ i ∈ I, f i a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, t < (fun x => ⨆ i ∈ I, f i x) x'