surjective_toEventualRanges — Mathlib

English

If F satisfies Mittag-Leffler, then its restriction to eventual ranges is a surjective functor; i.e., for any i ⟶ j, the map on eventual ranges is surjective.

Русский

Если F удовлетворяет условию Миттаг-Лефлера, то его ограничение на предельные диапазоны является сюръективным отображением; т.е. для любого ∇ i ⟶ j образ отображения на предельных диапазонах сюръективен.

LaTeX

$$$ (F.toEventualRanges.map f).Surjective $$$

Lean4

/-- If `F` satisfies the Mittag-Leffler condition, its restriction to eventual ranges is a
surjective functor. -/
theorem surjective_toEventualRanges (h : F.IsMittagLeffler) ⦃i j⦄ (f : i ⟶ j) : (F.toEventualRanges.map f).Surjective :=
  fun ⟨x, hx⟩ => by
  obtain ⟨y, hy, rfl⟩ := h.subset_image_eventualRange F f hx
  exact ⟨⟨y, hy⟩, rfl⟩

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