English
If there is a pointwise relation gb ∘ ϕ t = ϕ' t ∘ ga for all t and gb is continuous, then gb maps ω f ϕ s into ω f ϕ' s'.
Русский
Если gb ∘ ϕ t = ϕ' t ∘ ga для всех t и gb непрерывно, то 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 x, gb (ϕ t x) = ϕ' t (ga x))
(hgc : Continuous gb) : MapsTo gb (ω f ϕ s) (ω f ϕ' s') :=
mapsTo_omegaLimit' _ hs (Eventually.of_forall fun t x _hx ↦ hg t x) hgc
