no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type ?u.225648
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_2
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ←
  upperSemicontinuousWithinAt_univ_iff, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]