nullMeasurableSet_preimage_fst — Mathlib

English

For ν with ν ≠ 0, NullMeasurableSet (Prod.fst)⁻¹'(s) w.r.t. μ × ν is equivalent to NullMeasurableSet s w.r.t. μ.

Русский

Для ν ≠ 0, NullMeasurableSet (Prod.fst)⁻¹'(s) относительно μ × ν эквивалентно NullMeasurableSet s относительно μ.

LaTeX

$$$[\\text{NeZero } ν] \\; \\text{NullMeasurableSet}(\\text{preimage}(\\text{Prod.fst})(s)) (μ \\prod ν) \\iff \\text{NullMeasurableSet}(s) μ$$$

Lean4

/-- `Prod.fst ⁻¹' s` is null measurable w.r.t. `μ.prod ν` iff `s` is null measurable w.r.t. `μ`
provided that `ν ≠ 0`. -/
theorem nullMeasurableSet_preimage_fst [NeZero ν] {s : Set α} :
    NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν) ↔ NullMeasurableSet s μ :=
  ⟨.of_preimage_fst, (.preimage · quasiMeasurePreserving_fst)⟩

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