isLocallyFiniteMeasure — Mathlib

English

If all coordinate spaces have Topological structure and their volumes are NoAtoms, then the product volume is NoAtoms.

Русский

Если все координатные пространства имеют топологическую структуру и их объём/volume не содержит атомов, то объём произведения также не имеет атомов.

LaTeX

$$$\\text{NoAtoms}(\\text{volume}_{\\forall i})$$$

Lean4

instance isLocallyFiniteMeasure [∀ i, TopologicalSpace (α i)] [∀ i, IsLocallyFiniteMeasure (μ i)] :
    IsLocallyFiniteMeasure (Measure.pi μ) := by
  refine ⟨fun x => ?_⟩
  choose s hxs ho hμ using fun i => (μ i).exists_isOpen_measure_lt_top (x i)
  refine ⟨pi univ s, set_pi_mem_nhds finite_univ fun i _ => IsOpen.mem_nhds (ho i) (hxs i), ?_⟩
  rw [pi_pi]
  exact ENNReal.prod_lt_top fun i _ => hμ i

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