isMittagLeffler_iff_subset_range_comp

English

Let F be Mittag-Leffler with IsCofilteredOrEmpty J. Then F.IsMittagLeffler is equivalent to: for every j, there exists i and f : i ⟶ j such that for all g : k ⟶ i, range(F.map f) ⊆ range(F.map (g ≫ f)).

Русский

Пусть F удовлетворяет Mittag-Leffler в условиях IsCofilteredOrEmpty J. Тогда FIsMittagLeffler эквивалентно: для каждого j существует i и f: i ⟶ j такое, что для всех g : k ⟶ i, range(F.map f) ⊆ range(F.map (g ≫ f)).

LaTeX

$$$FIsMittagLeffler \iff \forall j, \exists i, f:\ i \to j, \forall k, g:\ k \to i,\ \mathrm{range}(F.map f) \subseteq \mathrm{range}(F.map (g \circ f)).$$$

Lean4

theorem isMittagLeffler_iff_subset_range_comp :
    F.IsMittagLeffler ↔ ∀ j : J, ∃ (i : _) (f : i ⟶ j), ∀ ⦃k⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map <| g ≫ f) :=
  by simp_rw [isMittagLeffler_iff_eventualRange, eventualRange_eq_iff]

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