frequently_sSup — Mathlib

English

For a set of filters fs, frequent on their supremum is equivalent to the existence of a filter f in fs which is frequent for p.

Русский

Частотность на наибольшем верхнем пределе множества фильтров равна существованию фильтра f в fs, для которого p часто выполняется.

LaTeX

$$$\\left(\\existsᶠ x\\in sSup\\,fs,\\ p(x)\\right) \\iff \\exists f \\in fs, \\existsᶠ x\\in f,\\ p(x)$$$

Lean4

@[simp]
theorem frequently_sSup {p : α → Prop} {fs : Set (Filter α)} : (∃ᶠ x in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ x in f, p x := by
  simp only [Filter.Frequently, not_forall, eventually_sSup, exists_prop]

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