English
Let l be a filter on α with HasBasis l p s. If P(t) holds for t eventually in l.smallSets, then there exists an index i with p(i) and P(s(i)).
Русский
Пусть l — фильтр на α, имеющий базис HasBasis l p s. Если свойство P(t) выполняется для множества t, удовлетворяющего условию малого множества l.smallSets, то существует индекс i такой, что p(i) и P(s(i)).
LaTeX
$$$\forall \alpha \ \forall \iota\ \forall l\, \forall p:\iota\to\mathrm{Prop}\forall s:\iota\to \mathcal P(\alpha)\forall P:\mathcal P(\alpha)\;\big( (\forall t\, t \in l.smallSets \Rightarrow P(t)) \land (HasBasis\ l\ p\ s) \Rightarrow \exists i, p(i) \land P(s(i)) \big)$$$
Lean4
theorem exists_mem_basis_of_smallSets {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop} (h₁ : ∀ᶠ t in l.smallSets, P t)
(h₂ : HasBasis l p s) : ∃ i, p i ∧ P (s i) :=
(h₂.smallSets.eventually_iff.mp h₁).imp fun _i ⟨hpi, hi⟩ ↦ ⟨hpi, hi Subset.rfl⟩
