t_isIso — Mathlib

English

Each morphism t i j is an isomorphism with inverse given by t j i and t i j relations; in particular, t i j is invertible for all i,j.

Русский

Каждый морфизм t i j является изоморфизмом, обратный ему задавается через t j i; для всех i,j выполняется инверсивность.

LaTeX

$$IsIso(D.t i j)$$

Lean4

instance t_isIso (i j : D.J) : IsIso (D.t i j) :=
  ⟨⟨D.t j i, D.t_inv _ _, D.t_inv _ _⟩⟩

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