Theorems · Theorem · category theory

CategoryTheory.Limits.Types.isLimit_iff

∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  (c : CategoryTheory.Limits.Cone F),
  Nonempty (CategoryTheory.Limits.IsLimit c) ↔
    ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x = s j

Defined in

Mathlib.CategoryTheory.Limits.Types.Limits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category