prod — Mathlib

English

If s and t are measurable sets, then s × t is measurable.

Русский

Если s и t — измеримые множества, то s × t измеримо.

LaTeX

$$$$ \operatorname{MeasurableSet}(s) \to \operatorname{MeasurableSet}(t) \to \operatorname{MeasurableSet}(s \times t) $$$$

Lean4

@[measurability]
theorem prod {f : α → β × γ} (hf₁ : Measurable fun a => (f a).1) (hf₂ : Measurable fun a => (f a).2) : Measurable f :=
  Measurable.of_le_map <|
    sup_le
      (by
        rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
        exact hf₁)
      (by
        rw [MeasurableSpace.comap_le_iff_le_map, MeasurableSpace.map_comp]
        exact hf₂)

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