comp_appTop — Mathlib

English

For morphisms f:X→Y, g:Y→Z, the appTop of the composition equals the composition of appTop maps: (f ≫ g).appTop = g.appTop ≫ f.appTop.

Русский

appTop композиции равен композиции appTop: (f ≫ g).appTop = g.appTop ≫ f.appTop.

LaTeX

$$$(f \\gg g).appTop = g.appTop \\circ f.appTop$$$

Lean4

@[simp, reassoc] -- reassoc lemma does not need `simp`

theorem comp_appTop {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).appTop = g.appTop ≫ f.appTop :=
  rfl

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