Theorems · Theorem · general topology

map_nhdsWithin

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] (f : α → β) (a : α) (s : Set α),
  Filter.map f (nhdsWithin a s) = ⨅ t ∈ {t | a ∈ t ∧ IsOpen t}, Filter.principal (f '' (t ∩ s))

Defined in

Mathlib.Topology.NhdsWithin

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace