Theorems · Theorem · category theory

CategoryTheory.Limits.ReflectsLimit.reflects

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsLimit K F] {c : CategoryTheory.Limits.Cone K}
  (hc : CategoryTheory.Limits.IsLimit (F.mapCone c)), Nonempty (CategoryTheory.Limits.IsLimit c)

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.ReflectsLimit