eventualRange_mapsTo — Mathlib

English

For any f : j ⟶ i, (F.eventualRange j) maps to (F.eventualRange i) along F.map f; i.e., every element of the eventual range at j maps into the eventual range at i.

Русский

Для любого f : j ⟶ i отображение F.map f отправляет F.eventualRange(j) в F.eventualRange(i).

LaTeX

$$$\forall x \in F.eventualRange(j),\ F.map f(x) \in F.eventualRange(i).$$$

Lean4

theorem eventualRange_mapsTo (f : j ⟶ i) : (F.eventualRange j).MapsTo (F.map f) (F.eventualRange i) := fun x hx =>
  by
  rw [mem_eventualRange_iff] at hx ⊢
  intro k f'
  obtain ⟨l, g, g', he⟩ := cospan f f'
  obtain ⟨x, rfl⟩ := hx g
  rw [← map_comp_apply, he, F.map_comp]
  exact ⟨_, rfl⟩

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