Theorems · Theorem · category theory

CategoryTheory.Functor.toEventualRanges_nonempty

∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [inst_1 : CategoryTheory.IsCofilteredOrEmpty J],
  F.IsMittagLeffler → ∀ [∀ (j : J), Nonempty (F.obj j)] (j : J), Nonempty (F.toEventualRanges.obj j)

If F is nonempty at each index and Mittag-Leffler, then so is F.toEventualRanges.

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmptyNonempty