nullMeasurable_comp_fst — Mathlib

English

For NeZero ν, null measurability of f ∘ fst with respect to μ × ν is equivalent to null measurability of f with respect to μ.

Русский

Для ν ≠ 0 нулевая измеримая композиция f ∘ fst относительно μ × ν эквивалентна нулевой измеримости f относительно μ.

LaTeX

$$$[\\text{NeZero } ν] \\; \\text{NullMeasurable}(f \\circ \\text{Prod.fst}) (μ \\prod ν) \\iff \\text{NullMeasurable}(f) μ$$$

Lean4

theorem nullMeasurable_comp_fst [NeZero ν] {f : α → γ} :
    NullMeasurable (f ∘ Prod.fst) (μ.prod ν) ↔ NullMeasurable f μ :=
  forall₂_congr fun s _ ↦ nullMeasurableSet_preimage_fst (s := f ⁻¹' s)

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