isMittagLeffler_iff_eventualRange

English

A functor F : J ⥤ Type v is Mittag-Leffler if and only if for every object j, there exist an object i and a morphism f : i ⟶ j such that F.eventualRange(j) = range(F.map f).

Русский

Функтор F : J ⥤ Type v удовлетворяет условию Mittag-Leffler тогда и только тогда, для каждого j существует объект i и морфизм f : i ⟶ j такой, что F.eventualRange(j) = range(F.map f).

LaTeX

$$$FIsMittagLeffler \iff \forall j : J, \exists i \; (f : i \to j), F.eventualRange(j) = \mathrm{range}(F.map f).$$$

Lean4

theorem isMittagLeffler_iff_eventualRange :
    F.IsMittagLeffler ↔ ∀ j : J, ∃ (i : _) (f : i ⟶ j), F.eventualRange j = range (F.map f) :=
  forall_congr' fun _ =>
    exists₂_congr fun _ _ => ⟨fun h => (iInter₂_subset _ _).antisymm <| subset_iInter₂ h, fun h => h ▸ iInter₂_subset⟩

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