of_preimage_fst — Mathlib

English

If s × t is null measurable for μ × ν and ν t ≠ 0, then s is null measurable with respect to μ.

Русский

Если s × t является нулевой измеримой для μ × ν и ν(t) ≠ 0, то s является нулевой измеримой относительно μ.

LaTeX

$$$\\text{NullMeasurableSet}(s \\timesˢ t) (μ \\prod ν) \\Rightarrow ν t ≠ 0 \\Rightarrow \\text{NullMeasurableSet}(s) μ$$$

Lean4

/-- If `Prod.fst ⁻¹' s` is a null measurable set and `ν ≠ 0`, then `s` is a null measurable set. -/
theorem _root_.MeasureTheory.NullMeasurableSet.of_preimage_fst [NeZero ν] {s : Set α}
    (h : NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν)) : NullMeasurableSet s μ :=
  .left_of_prod (by rwa [prod_univ]) (NeZero.ne (ν univ))

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