nullMeasurableSet_smul_measure_iff

English

For c ≠ 0, s is null-measurable under c • μ if and only if s is null-measurable under μ.

Русский

Для c ≠ 0 имеет место эквивалентность: nуль-измеримость s относительно μ и относительно c • μ совпадают.

LaTeX

$$NullMeasurableSet s (instHSMul.hSMul c μ) ↔ NullMeasurableSet s μ$$

Lean4

theorem nullMeasurableSet_smul_measure_iff {c : ℝ≥0∞} (hc : c ≠ 0) :
    NullMeasurableSet s (c • μ) ↔ NullMeasurableSet s μ :=
  ⟨fun h ↦ h.mono_ac (Measure.absolutelyContinuous_smul hc), fun h ↦ h.smul_measure c⟩

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