instGuitartExactOppositeOp — Mathlib

English

The property of Guitart exactness is preserved under taking opposites of the square.

Русский

Свойство точности Гитхарта сохраняется при взятии противоположного квадрата.

LaTeX

$$$w.GuitartExact\text{(op)} \iff w.GuitartExact$$$

Lean4

instance [w.GuitartExact] : w.op.GuitartExact :=
  by
  rw [guitartExact_iff_isConnected_rightwards]
  intro X₃ X₂ g
  rw [← isConnected_op_iff_isConnected, isConnected_iff_of_equivalence (w.structuredArrowRightwardsOpEquivalence g)]
  infer_instance

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