eq_image_eventualRange — Mathlib

English

If F is Mittag-Leffler, then for any f : j ⟶ i, the eventual range at i equals the image of F.map f on the eventual range at j.

Русский

Если F удовлетворяет условию Mittag-Leffler, то F.eventualRange(i) равно образу F.map f от F.eventualRange(j).

LaTeX

$$$FIsMittagLeffler \Rightarrow F.eventualRange(i) = \mathrm{image}(F.map f)(F.eventualRange(j)).$$$

Lean4

theorem eq_image_eventualRange (h : F.IsMittagLeffler) (f : j ⟶ i) : F.eventualRange i = F.map f '' F.eventualRange j :=
  (h.subset_image_eventualRange F f).antisymm <| mapsTo_iff_image_subset.1 (F.eventualRange_mapsTo f)

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