exists_mem_of_smallSets — Mathlib

English

Let p be a predicate on subsets of α. If p holds eventually on the family of small sets determined by the filter l, then there exists a set s that belongs to l such that p(s) holds.

Русский

Пусть p — предикат на подмножествax α. Если p выполняется в пределе на семействе малых множеств фильтра l, то существует множество s, принадлежащее фильтру l, такое что p(s) истинно.

LaTeX

$$$ \\forall p:\\\\mathcal P(\\\\alpha) \to \\mathrm{Prop},\\\\, (\\\\forall^\\\\infty t \\\\text{ in } l.smallSets, p(t)) \\\\Rightarrow \\\\exists s \\in l, p(s) $$$

Lean4

theorem exists_mem_of_smallSets {p : Set α → Prop} (h : ∀ᶠ t in l.smallSets, p t) : ∃ s ∈ l, p s :=
  h.exists_mem_basis_of_smallSets l.basis_sets

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