frequently_iSup — Mathlib

English

For a family fs of filters indexed by b, frequent on the iSup over b is equivalent to existence of an index b with p frequent in fs(b).

Русский

Частотность на iSup над b эквивалентна существованию индекса b, для которого p часто выполняется в fs(b).

LaTeX

$$$\\left(\\existsᶠ x\\in \\bigsqcup_{b} fs(b),\\ p(x)\\right) \\iff \\exists b,\\existsᶠ x\\in fs(b),\\ p(x)$$$

Lean4

@[simp]
theorem frequently_iSup {p : α → Prop} {fs : β → Filter α} : (∃ᶠ x in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ x in fs b, p x := by
  simp only [Filter.Frequently, eventually_iSup, not_forall]

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