no goals
α : Type u
t : TopologicalSpace α
⊢ ∀ (u : Set α), u ∈ {U | IsOpen U} → IsOpen u
tauto
no goals
α : Type u
t : TopologicalSpace α
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ {U | IsOpen U} ∧ a ∈ v ∧ v ⊆ u
tauto