homOfLE_apply — Mathlib

English

The app map on an open W agrees with the presheaf map induced by the corresponding LE-hom.

Русский

Отображение app на открытом W совпадает с отображением предшаблона, индуцированным соответствующим LE-гомом.

LaTeX

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

Lean4

@[simp]
theorem homOfLE_apply {U V : X.Opens} (e : U ≤ V) (x : U) : ((X.homOfLE e).base x).1 = x :=
  by
  rw [homOfLE_base]
  rfl

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