subset_image_eventualRange — Mathlib

English

If F is Mittag-Leffler and f : i ⟶ j, g : j ⟶ k with F.eventualRange k = range(F.map g), then F.eventualRange k = range(F.map (f ≫ g)).

Русский

Если F удовлетворяет условию Mittag-Leffler и f : i ⟶ j, g : j ⟶ k таковы, что F.eventualRange(k) = range(F.map g), то F.eventualRange(k) = range(F.map (f ≫ g)).

LaTeX

$$$F.eventualRange(k) = \mathrm{range}(F.map(g)) \Rightarrow F.eventualRange(k) = \mathrm{range}(F.map(f \circ g)).$$$

Lean4

theorem subset_image_eventualRange (h : F.IsMittagLeffler) (f : j ⟶ i) :
    F.eventualRange i ⊆ F.map f '' F.eventualRange j :=
  by
  obtain ⟨k, g, hg⟩ := F.isMittagLeffler_iff_eventualRange.1 h j
  rw [hg]; intro x hx
  obtain ⟨x, rfl⟩ := F.mem_eventualRange_iff.1 hx (g ≫ f)
  exact ⟨_, ⟨x, rfl⟩, by rw [map_comp_apply]⟩

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