homOfLE_appTop — Mathlib

English

The app map on the top open is the presheaf map corresponding to homOfLE restricted to top.

Русский

Отображение app на верхнем открытом множестве совпадает с отображением предшаблона, соответствующим homOfLE, ограниченным до верхнего уровня.

LaTeX

$$$ (X.homOfLE e).appTop = X.presheaf.map (homOfLE <| X.ι_image_homOfLE_le_ι_image e ⊤).op $$$

Lean4

theorem homOfLE_appTop {U V : X.Opens} (e : U ≤ V) :
    (X.homOfLE e).appTop = X.presheaf.map (homOfLE <| X.ι_image_homOfLE_le_ι_image e ⊤).op :=
  homOfLE_app ..

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