comp_c_app' — Mathlib

English

A variant of the previous statement at the opposite argument, expressing the same transport via op.

Русский

Вариант предыдущего утверждения для аргумента, находящегося в против числе.

LaTeX

$$$\forall X,Y,Z:\mathrm{SheafedSpace}(C),\; \alpha:X\to Y,\; \beta:Y\to Z,\; U:\mathrm{Opens}\;Z,\; (\alpha\circ\beta).c.app(\mathrm{op}\;U) = \beta.c.app(\mathrm{op}\;U) \circ \alpha.c.app(\mathrm{op}\left(\mathrm{Opens.map}\;\beta.base\;.obj\;U\right))$$$

Lean4

theorem comp_c_app' {X Y Z : SheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
    (α ≫ β).c.app (op U) = β.c.app (op U) ≫ α.c.app (op ((Opens.map β.base).obj U)) :=
  rfl

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