eventually_pi — Mathlib

English

If for every i, p i holds eventually in f i, then in the Pi-filter pi f, the property p i (x i) holds for all i simultaneously.

Русский

Если для каждого i свойство p i выполняется eventually в f i, тогда в фильтре Pi f выполняется p i (x i) для всех i вместе.

LaTeX

$$$\forall i, \forall^{\infty} x \in f_i,\ p i x \\Rightarrow \forall^{\infty} x : \forall i, \alpha_i \text{ in } \pi f, \forall i, p i (x_i).$$$

Lean4

theorem eventually_pi [Finite ι] (hf : ∀ i, ∀ᶠ x in f i, p i x) : ∀ᶠ x : ∀ i, α i in pi f, ∀ i, p i (x i) :=
  eventually_all.2 fun _i => (hf _).eval_pi

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