coconeOfConeLeftOp_ι_app — Mathlib

English

Reiterates the left-op cocone component correspondence with the opposite of the original cone projection.

Русский

Повторяет соответствие компонента кофана leftOp с противоположной проекцией исходного конуса.

LaTeX

$$$$ (\mathrm{coconeOfConeLeftOp}\, c).\iota_{j} = (c.\pi_{\mathrm{app}(\mathrm{op}\, j)})^{\mathrm{op}} $$$$

Lean4

@[simp]
theorem coconeOfConeLeftOp_ι_app (c : Cone F.leftOp) (j) : (coconeOfConeLeftOp c).ι.app j = (c.π.app (op j)).op :=
  by
  dsimp only [coconeOfConeLeftOp]
  simp

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