instNeBotUnconditional

Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

URI: https://scilib.ai/kg/mathlib#SummationFilter.instNeBotUnconditional

English

The unconditional filter on β is not bottom (NeBot).

Русский

Безусловный фильтр на β не является нижним (NeBot).

LaTeX

$$$\\text{NeBot}(\\text{unconditional }\\beta)$$$

Lean4

instance : (unconditional β).NeBot :=
  ⟨atTop_neBot⟩

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

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

Разделы

Аффилиация

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