omegaLimit_subset_of_tendsto — Mathlib

English

If m: τ → τ tends to f2 from f1, then ω f1 (t ↦ ϕ(t,·)) s ⊆ ω f2 ϕ s.

Русский

Если m: τ→τ сходится от f1 к f2, тогда ω-предел по f1 для s внутри ω-предела по f2.

LaTeX

$$$$\omega f_1 (\lambda t, x. ϕ(t, x)) \, s \subseteq \omega f_2 \; ϕ \; s.$$$$

Lean4

theorem omegaLimit_subset_of_tendsto {m : τ → τ} {f₁ f₂ : Filter τ} (hf : Tendsto m f₁ f₂) :
    ω f₁ (fun t x ↦ ϕ (m t) x) s ⊆ ω f₂ ϕ s :=
  by
  refine iInter₂_mono' fun u hu ↦ ⟨m ⁻¹' u, tendsto_def.mp hf _ hu, ?_⟩
  rw [← image2_image_left]
  exact closure_mono (image2_subset (image_preimage_subset _ _) Subset.rfl)

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