frequently

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Eventually.frequently

English

If a filter is nontrivial and p holds frequently, then p holds frequently.

Русский

Если фильтр не тождественно пуст, и p выполняется часто, то и p выполняется часто.

LaTeX

$$$ (\forall^\infty x \in f,\ p x) \rightarrow \exists^\infty x in f,\ p x $$$

Lean4

theorem frequently {f : Filter α} [NeBot f] {p : α → Prop} (h : ∀ᶠ x in f, p x) : ∃ᶠ x in f, p x :=
  compl_notMem h

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

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

Разделы

Аффилиация

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