measure_prod_compl_eq_zero — Mathlib

English

If s and t have μ(sᶜ) = 0 and ν(tᶜ) = 0, then μ × ν((s × t)ᶜ) = 0.

Русский

Если дополнения множеств s и t имеют нулевую меру, то дополнение множества s × t по произведению меры имеет нулевую меру.

LaTeX

$$μ.prod ν (s ×ˢ t)ᶜ = 0$$

Lean4

theorem measure_prod_compl_eq_zero {s : Set α} {t : Set β} (s_ae_univ : μ sᶜ = 0) (t_ae_univ : ν tᶜ = 0) :
    μ.prod ν (s ×ˢ t)ᶜ = 0 := by
  rw [Set.compl_prod_eq_union, measure_union_null_iff]
  simp [s_ae_univ, t_ae_univ]

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