English
For any predicate p on subsets, the statement that p holds eventually on l.smallSets is equivalent to the existence of a small set s in l such that p holds for all subsets t contained in s.
Русский
Для любого предиката p на подмножествa эквивалентно: p истинно на некоем малом множестве s в l, и тогда p применяется ко всем подмножествам t, удовлетворяющим t ⊆ s.
LaTeX
$$$ \\forall p:\\\\mathcal P(\\\\alpha) \\to \\\\mathrm{Prop}, \\\\ (\\\\forall^\\\\infty s \\\\in l.smallSets, p(s)) \\\\iff \\\\exists s \\in l, \\forall t, t \\subseteq s \\,\\to \\\\ p(t) $$$
Lean4
theorem eventually_smallSets {p : Set α → Prop} : (∀ᶠ s in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t, t ⊆ s → p t :=
eventually_lift'_iff monotone_powerset
