instNeBotValFilterCauchy

Mathlib.Topology.UniformSpace.Completion

URI: https://scilib.ai/kg/mathlib#CauchyFilter.instNeBotValFilterCauchy

English

A Cauchy filter on α has a nonempty underlying filter; i.e., its first component is nonempty.

Русский

У фильтра Коши на α непустое основание; то есть первый компонент филтра не пуст.

LaTeX

$$$\\forall f:\\nabla CauchyFilter(\\alpha),\\ NeBot\\, f.1$$$

Lean4

instance (f : CauchyFilter α) : NeBot f.1 :=
  f.2.1

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

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

Разделы

Аффилиация

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