fac_pull — Mathlib

English

Pullback identity for images: (A.pull θ).e ≫ image.ι (θ.unop ≫ A.e) = θ.unop ≫ A.e.

Русский

Идентичность обратного тяготения для изображений: (A.pull θ).e ≫ image.ι (θ.unop ≫ A.e) = θ.unop ≫ A.e.

LaTeX

$$$(A.pull\\ θ).e \\;\\gg\\; \\mathrm{image}.ι (\\theta.unop \\gg A.e) = \\theta.unop \\gg A.e$$$

Lean4

@[reassoc]
theorem fac_pull : (A.pull θ).e ≫ image.ι (θ.unop ≫ A.e) = θ.unop ≫ A.e :=
  image.fac _

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