instNoAtomsMixedSpaceVolume — Mathlib

English

The volume measure on the mixed space has no atoms.

Русский

Объемная мера на смешанном пространстве не имеет атомов.

LaTeX

$$$\mathrm{NoAtoms}(\mathrm{volume}).$$$

Lean4

instance : NoAtoms (volume : Measure (mixedSpace K)) :=
  by
  obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
  by_cases hw : IsReal w
  · have : NoAtoms (volume : Measure ({ w : InfinitePlace K // IsReal w } → ℝ)) := pi_noAtoms ⟨w, hw⟩
    exact prod.instNoAtoms_fst
  · have : NoAtoms (volume : Measure ({ w : InfinitePlace K // IsComplex w } → ℂ)) :=
      pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩
    exact prod.instNoAtoms_snd

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