isOpenPosMeasure — Mathlib

English

Let (μ_i) be a finite family of measures on spaces α_i, and assume each μ_i has the open-pos measure property. Then the product measure π μ on the finite product ∏_i α_i also has the open-pos measure property.

Русский

Пусть (μ_i) — конечная совокупность мер на пространства α_i, и пусть каждое μ_i обладает свойством открытости положительности. Тогда произведение π μ на конечном произведении ∏_i α_i тоже обладает свойством открытой положительности меры.

LaTeX

$$$\displaystyle \left(\forall i, \ IsOpenPosMeasure(\mu_i)\right) \Rightarrow IsOpenPosMeasure\bigl(\pi\,\mu\bigr)$$$

Lean4

instance isOpenPosMeasure [∀ i, TopologicalSpace (α i)] [∀ i, IsOpenPosMeasure (μ i)] :
    IsOpenPosMeasure (MeasureTheory.Measure.pi μ) := by
  constructor
  rintro U U_open ⟨a, ha⟩
  obtain ⟨s, ⟨hs, hsU⟩⟩ := isOpen_pi_iff'.1 U_open a ha
  refine ne_of_gt (lt_of_lt_of_le ?_ (measure_mono hsU))
  simp only [pi_pi]
  rw [CanonicallyOrderedAdd.prod_pos]
  intro i _
  apply (hs i).1.measure_pos (μ i) ⟨a i, (hs i).2⟩

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