singletonEquiv_symm_apply_self — Mathlib

English

The inverse of the singleton equivalence sends the element x back to x when applied to the identity at f.

Русский

Обратное к эквивалентности singleton возвращает элемент x на x при применении к тождественному отображению на f.

LaTeX

$$$(\\text{singletonEquiv } P f)^{-1} x \\, f \\, \\langle\\rangle = x$$$

Lean4

@[simp]
theorem singletonEquiv_symm_apply_self {X Y : C} (f : X ⟶ Y) (x : P.obj (op X)) :
    (singletonEquiv P f).symm x f ⟨⟩ = x := by simp [singletonEquiv_symm_apply]

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