English
For a finite countable set S of indices, the a.e. statement about all i ∈ S is equivalent to a family of a.e. statements for each i, uniform over S.
Русский
Для конечного множества индексов S, утверждение «для всех i∈S» почти верно эквивалентно совокупности утверждений для каждого i отдельно.
LaTeX
$$$S.Countable \to\n (\forall {p}, \forall a, \dots) \Leftrightarrow \dots$$$
Lean4
theorem ae_ball_iff {ι : Type*} {S : Set ι} (hS : S.Countable) {p : α → ∀ i ∈ S, Prop} :
(∀ᵐ x ∂μ, ∀ i (hi : i ∈ S), p x i hi) ↔ ∀ i (hi : i ∈ S), ∀ᵐ x ∂μ, p x i hi :=
eventually_countable_ball hS