ae_all_iff — Mathlib

English

For countable index set ι, and p : α → ι → Prop, a statement about ae for all i is equivalent to a family of ae statements for each i.

Русский

Пусть ι счётно; для p : α → ι → Prop справедливый эквивалент: p(a,i) выполняется а.я. для всех i ↔ для каждого i выполняется а.я.

LaTeX

$$$\bigl( \forall^{\text{ae}} a, \forall i, p(a,i) \bigr) \iff \forall i, \forall^{\text{ae}} a, p(a,i)$$$

Lean4

theorem ae_all_iff {ι : Sort*} [Countable ι] {p : α → ι → Prop} : (∀ᵐ a ∂μ, ∀ i, p a i) ↔ ∀ i, ∀ᵐ a ∂μ, p a i :=
  eventually_countable_forall

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