mathlib documentation

topology.category.Top.open_nhds

def topological_space.open_nhds {X : Top} (x : X) :
Type u

The type of open neighbourhoods of a point x in a (bundled) topological space.

Equations
@[instance]
Equations

The inclusion U ⊓ V ⟶ U as a morphism in the category of open sets.

Equations

The inclusion U ⊓ V ⟶ V as a morphism in the category of open sets.

Equations

The inclusion functor from open neighbourhoods of x to open sets in the ambient topological space.

Equations
@[simp]
@[simp]
theorem topological_space.open_nhds.map_id_obj' {X : Top} (x : X) (U : set X) (p : is_open U) (q : (𝟙 X) x U, p⟩) :
(topological_space.open_nhds.map (𝟙 X) x).obj U, p⟩, q⟩ = U, p⟩, q⟩
@[simp]
theorem is_open_map.functor_nhds_obj_coe {X Y : Top} {f : X Y} (h : is_open_map f) (x : X) (U : topological_space.open_nhds x) :
@[simp]
theorem is_open_map.functor_nhds_map {X Y : Top} {f : X Y} (h : is_open_map f) (x : X) (U V : topological_space.open_nhds x) (i : U V) :

An open map f : X ⟶ Y induces a functor open_nhds x ⥤ open_nhds (f x).

Equations

An open map f : X ⟶ Y induces an adjunction between open_nhds x and open_nhds (f x).

Equations