English
If p is a predicate on sets that is monotone with respect to inclusion, then eventual truth of p on l.smallSets implies existence of a small set s in l with p(s).
Русский
Если p — предикат на множества, монотонный по включению, тогда истинность p на малых множествах l.smallSets в пределе эквивалентна существованию малого множества s в l с p(s).
LaTeX
$$$ \\forall p:\\\\mathcal P(\\\\alpha) \\to \\\\mathrm{Prop}, (\\\\forall \\{s,t\\}, s \\\\subseteq t \\\\to p(t) \\\\to p(s)) \\\\Rightarrow \\\\big( (\\\\forall^\\\\infty s \\\\in l.smallSets, p(s)) \\\\iff \\\\exists s \\\\in l, p(s) \\big) $$$
Lean4
theorem eventually_smallSets' {p : Set α → Prop} (hp : ∀ ⦃s t⦄, s ⊆ t → p t → p s) :
(∀ᶠ s in l.smallSets, p s) ↔ ∃ s ∈ l, p s :=
eventually_smallSets.trans <| exists_congr fun s => Iff.rfl.and ⟨fun H => H s Subset.rfl, fun hs _t ht => hp ht hs⟩
