guitartExact_op_iff — Mathlib

English

The opposite square has Guitart exactness if and only if the original square does.

Русский

Противоположный квадрат обладает точностью Гитхарта тогда и только тогда, когда исходный квадрат обладает ей.

LaTeX

$$$w.op.GuitartExact \iff w.GuitartExact$$$

Lean4

theorem guitartExact_op_iff : w.op.GuitartExact ↔ w.GuitartExact :=
  by
  constructor
  · intro
    let w₁ : TwoSquare T (opOp C₁) (opOp C₂) T.op.op := 𝟙 _
    let w₂ : TwoSquare B.op.op (unopUnop C₃) (unopUnop C₄) B := 𝟙 _
    have : w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂ := by cat_disch
    rw [this]
    infer_instance
  · intro
    infer_instance

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