not_frequently

Mathlib.Order.Filter.Basic

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

English

Not frequently p is equivalent to eventually not p.

Русский

Не частотность p эквивалентна тому, что p не выполняется в пределе.

LaTeX

$$$ \neg \exists^\! x \in f, p(x) \iff \exists^\! x \in f, \neg p(x) $$$

Lean4

@[simp]
theorem not_frequently {p : α → Prop} {f : Filter α} : (¬∃ᶠ x in f, p x) ↔ ∀ᶠ x in f, ¬p x := by
  simp only [Filter.Frequently, not_not]

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

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

Разделы

Аффилиация

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