frequently_smallSets — Mathlib

English

If l has a basis and q is monotone, then frequently p(s) on smallSets is equivalent to p(s_i) for all i with p(i).

Русский

Если у l есть база и q монотонно, то часто p(s) на smallSets эквивалентно p(s_i) для всех i с p(i).

LaTeX

$$$ \\forall {\\alpha} {\\iota} {p} {l} {s} {q} {hl}, (\\\\forall ⦃s t⦄, s \\subseteq t \\to q t \\to q s) \\\\Rightarrow (\\\\forall^\\\\infty s \\\\in l.smallSets, q s) \\\\iff \\\\exists i, p i \\land q(s i))$$$

Lean4

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

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