eventually_all — Mathlib

English

If a finite index set is considered, then the statement that for all i, p_i holds eventually is equivalent to the conjunction of the individual eventualities: for each i, p_i holds eventually.

Русский

Если индексный набор конечен, то утверждение «для всех i выполняется eventually p_i» равно конъюнкции отдельных eventually p_i.

LaTeX

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

Lean4

@[simp]
theorem eventually_all {ι : Sort*} [Finite ι] {l} {p : ι → α → Prop} :
    (∀ᶠ x in l, ∀ i, p i x) ↔ ∀ i, ∀ᶠ x in l, p i x := by simpa only [Filter.Eventually, setOf_forall] using iInter_mem

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