pi_eval_preimage_null — Mathlib

English

If μ_i(s) = 0 for some i and set s ⊆ α_i, then the product measure of the preimage under eval_i is zero.

Русский

Если для некоторого i множество s имеет μ_i(s) = 0, то мера произведения на предобраз eval_i^{-1}(s) равна нулю.

LaTeX

$$$\mu_i(s) = 0 \Rightarrow \operatorname{Measure}(\pi\mu)(\operatorname{eval}_i^{-1}(s)) = 0$$$

Lean4

theorem pi_eval_preimage_null {i : ι} {s : Set (α i)} (hs : μ i s = 0) : Measure.pi μ (eval i ⁻¹' s) = 0 := by
  classical
    -- WLOG, `s` is measurable

  rcases exists_measurable_superset_of_null hs with ⟨t, hst, _, hμt⟩
  suffices Measure.pi μ (eval i ⁻¹' t) = 0 from measure_mono_null (preimage_mono hst) this
  rw [← univ_pi_update_univ, pi_pi]
  apply Finset.prod_eq_zero (Finset.mem_univ i)
  simp [hμt]

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