isLimitEquivSections_symm_apply — Mathlib

English

The inverse map sends a section x to the unique element whose projections equal x(j) for each j.

Русский

Обратное отображение отправляет секцию x в уникальный элемент x' с такими проекциями, что c.π.app j x' = x(j).

LaTeX

$$$(isLimitEquivSections t).symm x \\; \\text{ satisfies }\\; c.\\pi_{j}((isLimitEquivSections t).symm x) = x(j).$$$

Lean4

@[simp]
theorem isLimitEquivSections_symm_apply {c : Cone F} (t : IsLimit c) (x : F.sections) (j : J) :
    c.π.app j ((isLimitEquivSections t).symm x) = (x : ∀ j, F.obj j) j :=
  by
  conv_rhs => rw [← (isLimitEquivSections t).right_inv x]
  rfl

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