tendsto_const_nhds

Mathlib.Topology.Neighborhoods

URI: https://scilib.ai/kg/mathlib#tendsto_const_nhds

English

The constant function tends to its value in the neighborhood of that value.

Русский

Пусть константная функция принимает значение x; она стремится к x в окрестностях x.

LaTeX

$$$\\text{Tendsto } (\\lambda _ : \\mathcal{A}, x)\\ f\\ (𝓝 x).$$$

Lean4

theorem tendsto_const_nhds {f : Filter α} : Tendsto (fun _ : α => x) f (𝓝 x) :=
  tendsto_nhds.mpr fun _ _ ha => univ_mem' fun _ => ha

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru