pi_noAtoms — Mathlib

English

The a.e. equality transfers from Ioc to Icc in the product space.

Русский

Ae-равенство переносится из Ioc в Icc в произведении.

LaTeX

$$$ (\\mathrm{pi}\\; s\\; (\\lambda i.\\; \\mathrm{Ioc}(f_i))) =_{a.e.}^{\\mathrm{Measure.pi}\\; \\mu} \\mathrm{pi}\\; s\\; (\\lambda i.\\; \\mathrm{Icc}(f_i))$$$

Lean4

/-- If one of the measures `μ i` has no atoms, them `Measure.pi µ`
has no atoms. The instance below assumes that all `μ i` have no atoms. -/
theorem pi_noAtoms (i : ι) [NoAtoms (μ i)] : NoAtoms (Measure.pi μ) :=
  ⟨fun x => flip measure_mono_null (pi_hyperplane μ i (x i)) (singleton_subset_iff.2 rfl)⟩

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