leMapTop — Mathlib

English

There is a natural inclusion morphism U → (map f).obj ⊤ in Opens X; as a poset morphism this is the usual inclusion U ≤ (map f).obj ⊤.

Русский

Существуют естественный морфизм включения U → (map f).obj ⊤ в Opens X; как морфизм частичного порядка это обычное включение U ≤ (map f).obj ⊤.

LaTeX

$$$\\text{leMapTop}(f)(U) : U \\to (\\mathrm{map} f).\\mathrm{obj} \\top$, i.e. $U \\le (\\mathrm{map} f).\\mathrm{obj} \\top$$$

Lean4

/-- The inclusion `U ⟶ (map f).obj ⊤` as a morphism in the category of open sets.
-/
noncomputable def leMapTop (f : X ⟶ Y) (U : Opens X) : U ⟶ (map f).obj ⊤ :=
  leTop U

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