adjunctionNhds — Mathlib

English

There is an adjunction between OpenNhds.map f x and the functor IsInduced nhds x for inducing f, for each x.

Русский

Существуют адъюнкции между OpenNhds.map f x и функцией OpenNhds x для индуцирования f.

LaTeX

$$$OpenNhds.map\ f\ x \dashv OpenNhds\; x$ (для IsInducing f)$$

Lean4

/-- An inducing map `f : X ⟶ Y` induces an adjunction between `open_nhds x` and `open_nhds (f x)`.
-/
def adjunctionNhds (h : IsInducing f) (x : X) : OpenNhds.map f x ⊣ h.functorNhds x
    where
  unit := { app := fun U => homOfLE (h.adjunction.unit.app U.1).le }
  counit := { app := fun U => homOfLE (h.adjunction.counit.app U.1).le }

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