eventually_nhds_zero_mapsTo — Mathlib

English

If s ∈ 𝔖 and U is a neighborhood of 0 in F, then there exists a neighborhood of 0 in UniformConvergenceCLM σ F 𝔖 such that every f in that neighborhood maps s into U.

Русский

Пусть s ∈ 𝔖 и U — окрестность 0 в F. Тогда существует окрестность 0 в UniformConvergenceCLM σ F 𝔖, такая что для всех f из этой окрестности f(s) ⊆ U.

LaTeX

$$$$ \forall hs \in \mathfrak{S},\ U \in \mathcal{N}(0) : \\ \exists V \in 𝓝(0),\ \forall f \in V:\ MapsTo(f, s, U). $$$$

Lean4

theorem eventually_nhds_zero_mapsTo [TopologicalSpace F] [IsTopologicalAddGroup F] {𝔖 : Set (Set E)} {s : Set E}
    (hs : s ∈ 𝔖) {U : Set F} (hu : U ∈ 𝓝 0) : ∀ᶠ f : UniformConvergenceCLM σ F 𝔖 in 𝓝 0, MapsTo f s U :=
  by
  rw [nhds_zero_eq]
  apply_rules [mem_iInf_of_mem, mem_principal_self]

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