isoMk₀ — Mathlib

English

There is an isomorphism construction for ComposableArrows at level 0, built from a single isomorphism between the endpoints.

Русский

Существует конструктор изоморфизмов для ComposableArrows на уровне 0, построенный из изоморфизма концов.

LaTeX

$$$\text{isoMk}^0 : (e : F.obj'0 ≅ G.obj'0) \to (F \cong G)$$$

Lean4

/-- Constructor for isomorphisms in `ComposableArrows C 0`. -/
@[simps!]
def isoMk₀ {F G : ComposableArrows C 0} (e : F.obj' 0 ≅ G.obj' 0) : F ≅ G
    where
  hom := homMk₀ e.hom
  inv := homMk₀ e.inv

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