zero_zeroAtFilter

Mathlib.Order.Filter.ZeroAndBoundedAtFilter

URI: https://scilib.ai/kg/mathlib#Filter.zero_zeroAtFilter

English

The zero function tends to zero along any filter.

Русский

Нулевой функция сходит к нулю вдоль любого фильтра.

LaTeX

$$$\\mathrm{ZeroAtFilter}(l, 0)$$$

Lean4

theorem zero_zeroAtFilter [Zero β] [TopologicalSpace β] (l : Filter α) : ZeroAtFilter l (0 : α → β) :=
  tendsto_const_nhds

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

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

Разделы

Аффилиация

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