Equations
- topological_space.open_nhds x = {U // x ∈ U}
@[instance]
Equations
- topological_space.open_nhds.open_nhds_category x = _.mpr (category_theory.full_subcategory (λ (U : topological_space.opens ↥X), x ∈ U))
Equations
@[simp]
theorem
topological_space.open_nhds.inclusion_obj
{X : Top}
(x : X.α)
(U : topological_space.opens ↥X)
(p : x ∈ U) :
(topological_space.open_nhds.inclusion x).obj ⟨U, p⟩ = U
Equations
- topological_space.open_nhds.map f x = {obj := λ (U : topological_space.open_nhds (⇑f x)), ⟨(topological_space.opens.map f).obj U.val, _⟩, map := λ (U V : topological_space.open_nhds (⇑f x)) (i : U ⟶ V), (topological_space.opens.map f).map i, map_id' := _, map_comp' := _}
@[simp]
theorem
topological_space.open_nhds.map_obj
{X Y : Top}
(f : X ⟶ Y)
(x : ↥X)
(U : topological_space.opens ↥Y)
(q : ⇑f x ∈ U) :
(topological_space.open_nhds.map f x).obj ⟨U, q⟩ = ⟨(topological_space.opens.map f).obj U, q⟩
@[simp]
theorem
topological_space.open_nhds.map_id_obj
{X : Top}
(x : ↥X)
(U : topological_space.open_nhds (⇑(𝟙 X) x)) :
(topological_space.open_nhds.map (𝟙 X) x).obj U = U
@[simp]
theorem
topological_space.open_nhds.map_id_obj_unop
{X : Top}
(x : ↥X)
(U : (topological_space.open_nhds x)ᵒᵖ) :
(topological_space.open_nhds.map (𝟙 X) x).obj (opposite.unop U) = opposite.unop U
@[simp]
theorem
topological_space.open_nhds.op_map_id_obj
{X : Top}
(x : ↥X)
(U : (topological_space.open_nhds x)ᵒᵖ) :
(topological_space.open_nhds.map (𝟙 X) x).op.obj U = U
Equations
- topological_space.open_nhds.inclusion_map_iso f x = category_theory.nat_iso.of_components (λ (U : topological_space.open_nhds (⇑f x)), {hom := 𝟙 ((topological_space.open_nhds.inclusion (⇑f x) ⋙ topological_space.opens.map f).obj U), inv := 𝟙 ((topological_space.open_nhds.map f x ⋙ topological_space.open_nhds.inclusion x).obj U), hom_inv_id' := _, inv_hom_id' := _}) _
@[simp]
@[simp]