eventually_all_finite — Mathlib

English

Let I be a finite set of indices. Then (∀ᶠ x in l, ∀ i ∈ I, p_i x) holds if and only if ∀ i ∈ I, ∀ᶠ x in l, p_i x.

Русский

Пусть I — конечное множество индексов. Тогда (∀ᶠ x в l, ∀ i ∈ I, p_i x) эквивалентно ∀ i ∈ I, ∀ᶠ x в l, 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_finite {ι} {I : Set ι} (hI : I.Finite) {l} {p : ι → α → Prop} :
    (∀ᶠ x in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ x in l, p i x := by
  simpa only [Filter.Eventually, setOf_forall] using biInter_mem hI

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