of_forall

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Frequently.of_forall

English

If p holds for all x, then p holds frequently with respect to any filter.

Русский

Если p истинно для всех x, то p истинно часто относительно любого фильтра.

LaTeX

$$$ (\forall x,\ p x) \rightarrow \text{Frequently} (\lambda x, p x) \ f $$$

Lean4

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

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

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

Разделы

Аффилиация

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