functorNhds — Mathlib

English

An inducing map f induces an adjunction between OpenNhds.map f x and the functor OpenNhds x, for every x.

Русский

Индуктивное отображение f индуцирует адъюнкцию между OpenNhds.map f x и OpenNhds x для каждого x.

LaTeX

$$$OpenNhds.map\ f\ x \dashv OpenNhds\; x$$$

Lean4

/-- An inducing map `f : X ⟶ Y` induces a functor `open_nhds x ⥤ open_nhds (f x)`. -/
@[simps]
def functorNhds (h : IsInducing f) (x : X) : OpenNhds x ⥤ OpenNhds (f x)
    where
  obj U := ⟨h.functor.obj U.1, (h.mem_functorObj_iff U.1).mpr U.2⟩
  map := h.functor.map

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