op — Mathlib · SciLib

English

A binary fan gives a binary cofan in the opposite category: the op of a binary fan yields a binary cofan with components the opposites of the original legs.

Русский

Бинарный фен задаёт бинарный кофанктор в противоположной категории: применение оператора оп к бинарному фану даёт бинарный кофан с компонентами противоположностей исходных рёбер.

LaTeX

$$$ \\text{op}(c) = \\text{BinaryCofan} (c.fst^{op}) (c.snd^{op}) $$$

Lean4

/-- A binary fan gives a binary cofan in the opposite category. -/
protected abbrev op (c : BinaryFan X Y) : BinaryCofan (op X) (op Y) :=
  .mk c.fst.op c.snd.op

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