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