nullMeasurableSet_preimage_snd — Mathlib

English

For NeZero μ, the statement NullMeasurable (Prod.snd⁻¹′ t) (μ.prod ν) is equivalent to NullMeasurable t ν.

Русский

При не нулевой μ эквивалентно нулевой измеримости Prod.snd⁻¹′ t относительно μ × ν и t относительно ν.

LaTeX

$$NullMeasurableSet (Prod.snd⁻¹' t) (μ.prod ν) ≡ NullMeasurableSet t ν$$

Lean4

/-- `Prod.snd ⁻¹' t` is null measurable w.r.t. `μ.prod ν` iff `t` is null measurable w.r.t. `ν`
provided that `μ ≠ 0`. -/
theorem nullMeasurableSet_preimage_snd [NeZero μ] {t : Set β} :
    NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν) ↔ NullMeasurableSet t ν :=
  ⟨.of_preimage_snd, (.preimage · quasiMeasurePreserving_snd)⟩

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