Theorems · Theorem · general topology

TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open

∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → ∀ {a : α} {u : Set α}, a ∈ u → IsOpen u → ∃ v ∈ b, a ∈ v ∧ v ⊆ u

Defined in

Mathlib.Topology.Bases

Cited by

58 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace