prod — Mathlib

English

If s and t are null-measurable with respect to μ and ν, then s × t is null-measurable with respect to μ × ν.

Русский

Если s и t являются нулево измеримыми относительно μ и ν, то s × t является нулево измеримой относительно μ × ν.

LaTeX

$$NullMeasurableSet(s × t, μ.prod ν)$$

Lean4

theorem _root_.MeasureTheory.NullMeasurableSet.prod {s : Set α} {t : Set β} (s_mble : NullMeasurableSet s μ)
    (t_mble : NullMeasurableSet t ν) : NullMeasurableSet (s ×ˢ t) (μ.prod ν) :=
  let ⟨s₀, mble_s₀, s_aeeq_s₀⟩ := s_mble
  let ⟨t₀, mble_t₀, t_aeeq_t₀⟩ := t_mble
  ⟨s₀ ×ˢ t₀, ⟨mble_s₀.prod mble_t₀, set_prod_ae_eq s_aeeq_s₀ t_aeeq_t₀⟩⟩

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