tendsto_const_nhdsWithin — Mathlib

English

If a ∈ s, the constant map to a tends to 𝓝[s] a from any filter on β.

Русский

Постоянное отображение в a сходится к 𝓝[s] a при любом фильтре на β, если a ∈ s.

LaTeX

$$$ a \in s \Rightarrow \operatorname{Tendsto}(\lambda \_ : \beta \mapsto a)\ l (\mathcal{N}_s(a)) $$$

Lean4

theorem tendsto_const_nhdsWithin {l : Filter β} {s : Set α} {a : α} (ha : a ∈ s) :
    Tendsto (fun _ : β => a) l (𝓝[s] a) :=
  tendsto_const_pure.mono_right <| pure_le_nhdsWithin ha

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