smallSets_of_forall_mem_basis — Mathlib

English

Let h1: for all i, p(i) implies P(s(i)); and h2: HasBasis l p s. Then P holds frequently along l.smallSets, i.e., ∃ᶠ t in l.smallSets, P(t).

Русский

Пусть h1: для всех i, если p(i) то P(s(i)); и h2: HasBasis l p s. Тогда P выполняется часто на l.smallSets, то есть существует последовательность часто встречающихся t таких, что P(t).

LaTeX

$$$\forall i,\ p(i) \to P(s(i)) \;\land\; HasBasis\ l\ p\ s \Rightarrow \exists^{\infty} t \in l.smallSets,\ P(t)$$$

Lean4

theorem smallSets_of_forall_mem_basis {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop} (h₁ : ∀ i, p i → P (s i))
    (h₂ : HasBasis l p s) : ∃ᶠ t in l.smallSets, P t :=
  h₂.smallSets.frequently_iff.mpr fun _ hi => ⟨_, Subset.rfl, h₁ _ hi⟩

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