opEquiv — Mathlib

English

Equivalences of LiftStruct for a square and the corresponding square in the opposite category.

Русский

Эквиваленции LiftStruct для квадрата и соответствующего квадрата в противоположной категории.

LaTeX

$$$opEquiv\ (sq) : LiftStruct\ sq \simeq LiftStruct\ sq.op$$$

Lean4

/-- Equivalences of `LiftStruct` for a square and the corresponding square
in the opposite category. -/
@[simps]
def opEquiv (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.op
    where
  toFun := op
  invFun := unop
  left_inv := by cat_disch
  right_inv := by cat_disch

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