frequently_sup — Mathlib

English

Frequent on the join of two filters is true exactly when it is frequent in one or the other filter.

Русский

Частотность на объединении двух фильтров равна частотности в одном из них.

LaTeX

$$$\\left(\\existsᶠ x\\in f \\sqcup g,\\ p(x)\\right) \\iff \\left(\\existsᶠ x\\in f,\\ p(x)\\right) \\lor \\left(\\existsᶠ x\\in g,\\ p(x)\\right)$$$

Lean4

theorem frequently_sup {p : α → Prop} {f g : Filter α} : (∃ᶠ x in f ⊔ g, p x) ↔ (∃ᶠ x in f, p x) ∨ ∃ᶠ x in g, p x := by
  simp only [Filter.Frequently, eventually_sup, not_and_or]

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