eventually_countable_ball — Mathlib

English

Let S be countable and p: α → ∀ i ∈ S, Prop. Then (∀ᶠ x in l, ∀ i hi, p x i hi) iff ∀ i hi, ∀ᶠ x in l, p x i hi.

Русский

Пусть S счётно, и p(x,i) задано на каждом i ∈ S. Тогда (∀ᶠ x, ∀ i ∈ S, p(x,i)) равносильно ∀ i ∈ S, ∀ᶠ x, p(x,i).

LaTeX

$$$\\Big( \\forall^{\\!\\infty}_{x\\to l} x \\Big) \\forall i, hi, p(x,i,hi) \\iff \\forall i, hi, \\forall^{\\!\\infty}_{x\\to l} p(x,i,hi)$$$

Lean4

theorem eventually_countable_ball {ι : Type*} {S : Set ι} (hS : S.Countable) {p : α → ∀ i ∈ S, Prop} :
    (∀ᶠ x in l, ∀ i hi, p x i hi) ↔ ∀ i hi, ∀ᶠ x in l, p x i hi := by
  simpa only [Filter.Eventually, setOf_forall] using @countable_bInter_mem _ l _ _ _ hS fun i hi => {x | p x i hi}

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