functorNhds — Mathlib

English

If f is an open map, then for each x, there is an adjunction between the functor OpenNhds x → OpenNhds (f x) obtained from the open map and the OpenNhds map along f.

Русский

Если f — открывающее отображение, то для каждого x существует скрытие между означенным функтором OpenNhds x → OpenNhds (f x) и OpenNhds.map f x.

LaTeX

$$$\text{IsOpenMap}.functorNhds\; f\; x \dashv OpenNhds.map\; f\; x$$$

Lean4

/-- An open map `f : X ⟶ Y` induces a functor `OpenNhds x ⥤ OpenNhds (f x)`. -/
@[simps]
def functorNhds (h : IsOpenMap f) (x : X) : OpenNhds x ⥤ OpenNhds (f x)
    where
  obj U := ⟨h.functor.obj U.1, ⟨x, U.2, rfl⟩⟩
  map i := h.functor.map i

Похожие утверждения