eventually_cardinal_forall — Mathlib

English

Let p: α → ι → Prop and hic: #ι < c. Then (∀ᶠ x in l, ∀ i, p(x,i)) is equivalent to ∀ i, ∀ᶠ x in l, p(x,i).

Русский

Пусть p: α → ι → Prop и #ι < c. Тогда (∀ᶠ x ∈ l) ∀ i p(x,i) эквивалентно ∀ i ∀ᶠ x ∈ l, p(x,i).

LaTeX

$$$(#ι < c) \\rightarrow \\Big( (\\forall^\\infty x \\in l, \\forall i, p(x,i)) \\Leftrightarrow \\forall i, \\forall^\\infty x \\in l, p(x,i) \\Big)$$$

Lean4

theorem eventually_cardinal_forall {p : α → ι → Prop} (hic : #ι < c) :
    (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i :=
  by
  simp only [Filter.Eventually, setOf_forall]
  exact cardinal_iInter_mem hic

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