of_preimage_snd — Mathlib

English

If μ ≠ 0 and Prod.snd⁻¹′ t is null-measurable w.r.t. μ × ν, then t is null-measurable w.r.t. ν.

Русский

Если μ ≠ 0 и Prod.snd⁻¹′ t нулево измеримо относительно μ × ν, тогда t нулево измеримо относительно ν.

LaTeX

$$NullMeasurableSet t ν$$

Lean4

/-- If `Prod.snd ⁻¹' t` is a null measurable set and `μ ≠ 0`, then `t` is a null measurable set. -/
theorem _root_.MeasureTheory.NullMeasurableSet.of_preimage_snd [NeZero μ] {t : Set β}
    (h : NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)) : NullMeasurableSet t ν :=
  .right_of_prod (by rwa [univ_prod]) (NeZero.ne (μ univ))

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