ae_pi_le_pi — Mathlib

English

Almost everywhere on the product is contained in the product of a.e. sets on each factor.

Русский

Почти всюду на произведении содержится произведение множеств с а.е. на каждой компоненте.

LaTeX

$$$\operatorname{ae}(\pi\mu) \leq \operatorname{Filter.pi}(i \mapsto \operatorname{ae}(\mu_i))$$$

Lean4

theorem ae_pi_le_pi : ae (Measure.pi μ) ≤ Filter.pi fun i => ae (μ i) :=
  le_iInf fun _ => tendsto_eval_ae_ae.le_comap

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