eventually_cardinal_ball — Mathlib

English

Let S ⊆ ι with #S < c and p: α → ∀ i ∈ S, Prop. Then (∀ᶠ x, ∀ i hi, p x i hi) is equivalent to ∀ i hi, ∀ᶠ x, p x i hi.

Русский

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

LaTeX

$$$#S < c \\rightarrow (\\forall x \\in l, \\forall i \\in S, \\forall hi, p(x,i,hi)) \\Leftrightarrow \\forall i \\in S, \\forall hi, \\forall x \\in l, p(x,i,hi)$$$

Lean4

theorem eventually_cardinal_ball {S : Set ι} (hS : #S < c) {p : α → ∀ i ∈ S, Prop} :
    (∀ᶠ x in l, ∀ i hi, p x i hi) ↔ ∀ i hi, ∀ᶠ x in l, p x i hi :=
  by
  simp only [Filter.Eventually, setOf_forall]
  exact cardinal_bInter_mem hS

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