eventually_all_finset — Mathlib

English

For a Finset I, (∀ᶠ x in l, ∀ i ∈ I, p_i x) is equivalent to ∀ i ∈ I, ∀ᶠ x in l, p_i x.

Русский

Для Finset I эквивалентно: (∀ᶠ x, ∀ i ∈ I, p_i x) ↔ ∀ i ∈ I, ∀ᶠ x, p_i x.

LaTeX

$$$ (\forall^{\!} x \in l, \forall i \in I, p_i x) \iff \forall i \in I, (\forall^{\!} x \in l, p_i x) $$$

Lean4

@[simp]
theorem eventually_all_finset {ι} (I : Finset ι) {l} {p : ι → α → Prop} :
    (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ x in l, p i x :=
  I.finite_toSet.eventually_all

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