frequently_iff — Mathlib

English

For a HasBasis l with p s, the statement that q holds frequently in l is equivalent to: for every i with p i there exists x in s i with q x.

Русский

Для HasBasis l с p и s утверждение о частотности q эквивалентно: для каждого i с p i существует x в s i такое, что q x.

LaTeX

$$$l\text{ HasBasis } p s \;\Rightarrow\; (\exists \text{freq } x\in l, q x) \Leftrightarrow \forall i, p i \rightarrow \exists x\in s i, q x$$$

Lean4

theorem frequently_iff (hl : l.HasBasis p s) {q : α → Prop} : (∃ᶠ x in l, q x) ↔ ∀ i, p i → ∃ x ∈ s i, q x := by
  simp only [Filter.Frequently, hl.eventually_iff]; push_neg; rfl

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