tendsto_iff_tendstoUniformlyOn — Mathlib

English

If f is a uniform embedding, then the postcomposition map is a uniform embedding between the corresponding 𝔖-convergence spaces.

Русский

Если f — равномерное вложение, то отображение по пост-композиции является равномерным вложением между 𝔖-конвергенциями.

LaTeX

$$IsUniformEmbedding f → IsUniformEmbedding (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖).$$

Lean4

/-- Convergence in the topology of `𝔖`-convergence means uniform convergence on `S` (in the sense
of `TendstoUniformlyOn`) for all `S ∈ 𝔖`. -/
protected theorem tendsto_iff_tendstoUniformlyOn {F : ι → α →ᵤ[𝔖] β} {f : α →ᵤ[𝔖] β} :
    Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (toFun 𝔖 ∘ F) (toFun 𝔖 f) p s := by
  simp only [UniformOnFun.nhds_eq, tendsto_iInf, tendsto_principal, TendstoUniformlyOn, Function.comp_apply, mem_setOf]

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