Theorems · Theorem · category theory

CategoryTheory.Limits.Types.limitEquivSections_symm_apply

∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasLimit F] (x : ↑F.sections) (j : J),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j))
      ((CategoryTheory.Limits.Types.limitEquivSections F).symm x) =
    ↑x j

Defined in

Mathlib.CategoryTheory.Limits.Types.Limits

Cited by

1 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasLimit