no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type ?u.229144
inst✝³ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
γ : Type u_2
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
simp_rw [continuous_iff_continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn,
  lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff]