interUnionPullbackCone_fst — Mathlib

English

The pullback cone is defined by the two maps $F(U) \\leftarrow F(U \\cup V) \\rightarrow F(V)$ induced by the restriction maps along inclusions, giving the pullback over $F(U \\cap V)$.

Русский

Конус-пуллбэк определяется двумя отображениями от F(U ⊔ V) к F(U) и к F(V), индуцированными ограничениями по вложениям, образуя пуллбэк над F(U ∩ V).

LaTeX

$$$\\text{interUnionPullbackCone} : PullbackCone( F.1.map( homOfLE inf\\_le\\_left ).op, F.1.map( homOfLE inf\\_le\\_right ).op )$$$

Lean4

@[simp]
theorem interUnionPullbackCone_fst : (interUnionPullbackCone F U V).fst = F.1.map (homOfLE le_sup_left).op :=
  rfl

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