no goals
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
hl : ∃ l, l < a
hu : ∃ u, a < u
s : Set α
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) ↔ ∃ i, (i.fst < a ∧ a < i.snd) ∧ Ioo i.fst i.snd ⊆ s
simp