α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.117874
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.117903
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') univ x
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.117874
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.117903
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' => ⨆ (i : ι), f i x') x
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.117874
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.117903
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[univ] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') univ x
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.117874
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.117903
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') univ x
rw [← nhdsWithin_univ] at bdd
no goals
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.117874
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type ?u.117903
δ' : Type u_2
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[univ] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (i : ι), f i x') univ x
exact lowerSemicontinuousWithinAt_ciSup bdd h