Theorems · Theorem · general topology

Filter.HasBasis.hasBasis_of_isDenseInducing

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [RegularSpace β]
  {ι : Type u_5} {s : ι → Set α} {p : ι → Prop} {x : α},
  (nhds x).HasBasis p s → ∀ {f : α → β}, IsDenseInducing f → (nhds (f x)).HasBasis p fun i => closure (f '' s i)

Defined in

Mathlib.Topology.DenseEmbedding

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceRegularSpace