inv_fst — Mathlib

English

The fst component of the inverse of a morphism equals the inverse of the fst component.

Русский

Компонента fst в противоположном морфизме совпадает с обратной компонентой fst.

LaTeX

$$$ (inv f).fst = inv (f.fst) $$$

Lean4

@[simp]
theorem inv_fst : (inv f).fst = inv f.fst := by
  symm
  apply IsIso.inv_eq_of_hom_inv_id
  simpa [-IsIso.hom_inv_id] using congrArg (fun t ↦ t.fst) (IsIso.hom_inv_id f)

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