ae_ball_iff — Mathlib

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

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