no goals
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ LowerSemicontinuousOn f univ ↔ LowerSemicontinuous f
simp [LowerSemicontinuousOn, LowerSemicontinuous, lowerSemicontinuousWithinAt_univ_iff]