English
If there is a map ga: α → α' sending s into s' and gb: β → β' continuous, with eventual equality of gb ∘ ϕ t and ϕ' t ∘ ga on s, then gb maps ω f ϕ s into ω f ϕ' s'.
Русский
Если существует отображение ga: α → α', которое отправляет s в s', и gb: β → β' непрерывно, причем gb ∘ ϕ t и ϕ' t ∘ ga совпадают на s на большинстве t, то gb отображает ω f ϕ s в ω f ϕ' s'.
LaTeX
$$$$\text{mapsTo } gb\; (\omega f\, ϕ\, s)\; (\omega f\, ϕ'\, s').$$$$
Lean4
theorem mapsTo_omegaLimit' {α' β' : Type*} [TopologicalSpace β'] {f : Filter τ} {ϕ : τ → α → β} {ϕ' : τ → α' → β'}
{ga : α → α'} {s' : Set α'} (hs : MapsTo ga s s') {gb : β → β'} (hg : ∀ᶠ t in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s)
(hgc : Continuous gb) : MapsTo gb (ω f ϕ s) (ω f ϕ' s') :=
by
simp only [omegaLimit_def, mem_iInter, MapsTo]
intro y hy u hu
refine map_mem_closure hgc (hy _ (inter_mem hu hg)) (forall_mem_image2.2 fun t ht x hx ↦ ?_)
calc
ϕ' t (ga x) ∈ image2 ϕ' u s' := mem_image2_of_mem ht.1 (hs hx)
_ = gb (ϕ t x) := ht.2 hx |>.symm
