α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s
rw [t.topology_eq_generate_intervals]
no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s
rfl