tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within

English

Let a ∈ α, l a filter on β, s ⊆ α, and f: β → α. If f tends to a along l in the whole space and f eventually lies in s, then f tends to a within s.

Русский

Пусть a ∈ α, l фильтр на β, s ⊆ α и f: β → α. Если f стремится к a по всему пространству и в большинстве случаев f лежит в s, тогда f стремится внутри s к a.

LaTeX

$$$ f:\\beta \\to α,\\ h1: Tendsto f l (\\mathcal{N} a),\\ h2: (\\forall^\\infty x \\in l, f x \\in s) \\Rightarrow Tendsto f l (\\mathcal{N} [s] a) $$$

Lean4

theorem tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within {a : α} {l : Filter β} {s : Set α} (f : β → α)
    (h1 : Tendsto f l (𝓝 a)) (h2 : ∀ᶠ x in l, f x ∈ s) : Tendsto f l (𝓝[s] a) :=
  tendsto_inf.2 ⟨h1, tendsto_principal.2 h2⟩

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