eventually_countable_forall — Mathlib

English

For Countable ι, (∀ᶠ x in l, ∀ i, p x i) iff ∀ i, ∀ᶠ x in l, p x i.

Русский

Для счетного ι, (∀ᶠ x, ∀ i, p(x,i)) эквивалентно ∀ i, ∀ᶠ x, p(x,i).

LaTeX

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

Lean4

theorem eventually_countable_forall [Countable ι] {p : α → ι → Prop} :
    (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i := by
  simpa only [Filter.Eventually, setOf_forall] using @countable_iInter_mem _ _ l _ _ fun i => {x | p x i}

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