adjunctionNhds — Mathlib

English

An open map f induces an adjunction between the functor Nhds_h x and the OpenNhds.map f x for each x.

Русский

Открывающее отображение f порождает адъюнкцию между функтором Nhds_x и OpenNhds.map f x для каждого x.

LaTeX

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

Lean4

/-- An open map `f : X ⟶ Y` induces an adjunction between `OpenNhds x` and `OpenNhds (f x)`. -/
def adjunctionNhds (h : IsOpenMap f) (x : X) : IsOpenMap.functorNhds h x ⊣ OpenNhds.map f x
    where
  unit := { app := fun _ => homOfLE fun x hxU => ⟨x, hxU, rfl⟩ }
  counit := { app := fun _ => homOfLE fun _ ⟨_, hfxV, hxy⟩ => hxy ▸ hfxV }

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