instNoAtomsForallVolumeOfNonemptyOfSigmaFinite

English

If ι is nonempty, and every μ_i is a measure with NoAtoms, then the product measure on ∀ i is also NoAtoms.

Русский

Если ι непустое и каждая μ_i имеет NoAtoms, то произведение мер тоже не имеет атомов.

LaTeX

$$$\\text{NoAtoms}(\\mathrm{Measure.pi}\\; μ)$$$

Lean4

instance {α : ι → Type*} [Nonempty ι] [∀ i, MeasureSpace (α i)] [∀ i, SigmaFinite (volume : Measure (α i))]
    [∀ i, NoAtoms (volume : Measure (α i))] : NoAtoms (volume : Measure (∀ i, α i)) :=
  pi_noAtoms'

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