pi_noAtoms' — Mathlib

English

If at least one index is present, and each component measure has no atoms, then the product measure on the Pi-space has no atoms.

Русский

Если существует хотя бы один индекс и каждая мера без атомов, то произведение меры на пространстве Pi не имеет атомов.

LaTeX

$$$\\text{NoAtoms}(\\mathrm{Measure.pi}\\; \\mu)$ under assumptions$$

Lean4

instance pi_noAtoms' [h : Nonempty ι] [∀ i, NoAtoms (μ i)] : NoAtoms (Measure.pi μ) :=
  h.elim fun i => pi_noAtoms i

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