no goals
α : Type u_1
inst✝³ : TopologicalSpace α
β : Type ?u.128024
inst✝² : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Sort u_3
δ : Type u_2
δ' : Type ?u.128056
inst✝¹ : CompleteLinearOrder δ
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuous (f i)
⊢ ∀ (x : α), BddAbove (range fun i => f i x)
simp