not_eventually

Mathlib.Order.Filter.Basic

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

English

Not eventually p is equivalent to frequently not p.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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