mathlib documentation

topology.category.Top.open_nhds

def topological_space.open_nhds {X : Top} :
X → Type u

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
@[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⟩