equiv_symm_ι_apply — Mathlib

English

The symmetric application of the equivalence sends the image under ι to the corresponding element in F.ιColimitType.

Русский

Симметричное применение эквивалентности переводит образ через ι к соответствующему элементу внутри F.ιColimitType.

LaTeX

$$$hc.equiv.symm (c.ι j x) = F.ιColimitType j x$$$

Lean4

@[simp]
theorem equiv_symm_ι_apply (j : J) (x : F.obj j) : hc.equiv.symm (c.ι j x) = F.ιColimitType j x :=
  hc.equiv.injective (by simp)

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