eventually_smallSets — Mathlib

English

If l has a basis {s_i} with p(i) and s_i and a monotone q, then p and q characterize eventual smallSets: there exists i with p(i) and q(s_i).

Русский

Если у фильтра l есть база {s_i} с p(i) и s_i, и задана монотонная функция q, то эвентуальная крошка smallSets описывается существованием i с p(i) и q(s_i).

LaTeX

$$$ \\forall i, p(i) \\land q(s(i)) \\text{ holds if } (\\\\forall^\\\\infty s \\\\in l.smallSets, q(s)) $ with hl : l.HasBasis p s$$

Lean4

theorem eventually_smallSets {α : Type*} {ι : Sort*} {p : ι → Prop} {l : Filter α} {s : ι → Set α} {q : Set α → Prop}
    {hl : l.HasBasis p s} (hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s) : (∀ᶠ s in l.smallSets, q s) ↔ ∃ i, p i ∧ q (s i) :=
  by rw [l.eventually_smallSets' hq, hl.exists_iff hq]

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