isLimitEquivSections_apply — Mathlib

English

The forward direction of the limit-equivalence maps x ∈ c.pt to the family of projections (∀ j, c.π.app j x).

Русский

Прямой образ изоморфизма из лимитирования отображает элемент x ∈ c.pt в семейство проекций (∀ j, c.π.app j x).

LaTeX

$$$(isLimitEquivSections\\ t\\ x) : \\forall j, F.obj j$ and $(isLimitEquivSections\\ t\\ x)(j) = c.\\pi_{j} x.$$$

Lean4

@[simp]
theorem isLimitEquivSections_apply {c : Cone F} (t : IsLimit c) (j : J) (x : c.pt) :
    (isLimitEquivSections t x : ∀ j, F.obj j) j = c.π.app j x :=
  rfl

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