α : Type u_1
β : Type ?u.3811
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, Ici aᶜ = t} s
α : Type u_1
β : Type ?u.3811
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, Ici aᶜ = t} s
rw [topology_eq α]
no goals
α : Type u_1
β : Type ?u.3811
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : LowerTopology α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, Ici aᶜ = t} s
rfl