interUnionPullbackCone_snd — Mathlib

English

The snd projection of the pullback cone is given by the restriction map from F(U ⊔ V) to F(V).

Русский

Вторая проекция конуса-пулбека равна отображению ограничения F(U ⊔ V) → F(V).

LaTeX

$$$(\\text{interUnionPullbackCone } F U V).snd = F.1.map( (\\mathrm{homOfLE}\\ inf\\_le\\_right) ).op$$$

Lean4

@[simp]
theorem interUnionPullbackCone_snd : (interUnionPullbackCone F U V).snd = F.1.map (homOfLE le_sup_right).op :=
  rfl

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