prod — Mathlib

English

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

Русский

Если s и t измеримы, то s × t измеримо.

LaTeX

$$$$ \operatorname{MeasurableSet}(s) \rightarrow \operatorname{MeasurableSet}(t) \rightarrow \operatorname{MeasurableSet}(s \times \! t) $$$$

Lean4

@[measurability]
protected theorem prod {s : Set α} {t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) : MeasurableSet (s ×ˢ t) :=
  MeasurableSet.inter (measurable_fst hs) (measurable_snd ht)

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