tendsto_const_pure — Mathlib

English

For any β and b ∈ β, Tendsto (const b) a (pure b) for any filter a on α.

Русский

Для любой β и b ∈ β, Tendsto (постоянная функция, принимающая значение b) a (pure b) для любого фильтра a на α.

LaTeX

$$$ \\operatorname{Tendsto} (\\lambda\\_x. b) a \\mathrm{pure}(b) $$$

Lean4

theorem tendsto_const_pure {a : Filter α} {b : β} : Tendsto (fun _ => b) a (pure b) :=
  tendsto_pure.2 <| univ_mem' fun _ => rfl

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