mk' — Mathlib

English

A constructor mk' provides a way to build a triangulated equivalence from a triangulated forward functor.

Русский

Конструктор mk' позволяет построить триангулированную эквивалентность из триангулированного прямого функторa.

LaTeX

$$$\text{mk}'(h): E.IsTriangulated \text{ where rightAdjoint_isTriangulated := ...}$$$

Lean4

/-- Constructor for `Equivalence.IsTriangulated`. -/
theorem mk' (h : E.functor.IsTriangulated) : E.IsTriangulated where
  rightAdjoint_isTriangulated := E.toAdjunction.isTriangulated_rightAdjoint

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