apply TopologicalSpace.isOpen_generateFrom_of_mem
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
⊢ IsOpen (Set.Ioc a (f c))
case hs
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
⊢ Set.Ioc a (f c) ∈ upper_intervals