English
For any f : i ⟶ j, eventualRange(j) = range(F.map f) iff for all k and g : k ⟶ i, range(F.map f) ⊆ range(F.map (g ≫ f)).
Русский
Для любого f : i ⟶ j, F.eventualRange(j) = range(F.map f) тогда и только тогда, когда для всех k и g : k ⟶ i, range(F.map f) ⊆ range(F.map (g ≫ f)).
LaTeX
$$$F.eventualRange(j) = \mathrm{range}(F.map f) \iff \forall k\; \forall g : k \to i,\ \mathrm{range}(F.map f) \subseteq \mathrm{range}(F.map (g \circ f)).$$$
Lean4
theorem eventualRange_eq_iff {f : i ⟶ j} :
F.eventualRange j = range (F.map f) ↔ ∀ ⦃k⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map <| g ≫ f) :=
by
rw [subset_antisymm_iff, eventualRange, and_iff_right (iInter₂_subset _ _), subset_iInter₂_iff]
refine ⟨fun h k g => h _ _, fun h j' f' => ?_⟩
obtain ⟨k, g, g', he⟩ := cospan f f'
refine (h g).trans ?_
rw [he, F.map_comp]
apply range_comp_subset_range
