eventualRange_eq_range_precomp — Mathlib

English

If F.eventualRange k equals the range of F.map g, then it also equals the range of F.map (f ≫ g) for any f.

Русский

Если F.eventualRange k совпадает с образами F.map g, тогда при любом f выполняется 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 eventualRange_eq_range_precomp (f : i ⟶ j) (g : j ⟶ k) (h : F.eventualRange k = range (F.map g)) :
    F.eventualRange k = range (F.map <| f ≫ g) :=
  by
  apply subset_antisymm
  · apply iInter₂_subset
  · rw [h, F.map_comp]
    apply range_comp_subset_range

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