op — Mathlib · SciLib

English

The commutative square in the opposite category associated to a commutative square.

Русский

Коммутативный квадрат в противоположной категории, связанный с данным коммутативным квадратом.

LaTeX

$$theorem op (p : CommSq f g h i) : CommSq i.op h.op g.op f.op$$

Lean4

/-- The commutative square in the opposite category associated to a commutative square. -/
theorem op (p : CommSq f g h i) : CommSq i.op h.op g.op f.op :=
  ⟨by simp only [← op_comp, p.w]⟩

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