nullMeasurable_comp_snd — Mathlib

English

For any measurable f: β → γ, NullMeasurable (f ∘ Prod.snd) (μ.prod ν) is equivalent to NullMeasurable f ν.

Русский

Для любого измеримого f: β → γ, NullMeasurable (f ∘ Prod.snd) (μ.prod ν) эквивалентно NullMeasurable f ν.

LaTeX

$$NullMeasurable (f ∘ Prod.snd) (μ.prod ν) ↔ NullMeasurable f ν$$

Lean4

theorem nullMeasurable_comp_snd [NeZero μ] {f : β → γ} :
    NullMeasurable (f ∘ Prod.snd) (μ.prod ν) ↔ NullMeasurable f ν :=
  forall₂_congr fun s _ ↦ nullMeasurableSet_preimage_snd (t := f ⁻¹' s)

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