English
Let s ⊆ α and t ⊆ β be sets with (s × t) ≠ ∅. Then s × t is a measurable set if and only if s and t are measurable individually.
Русский
Пусть s ⊆ α и t ⊆ β. если множество произведения s × t непустое, то оно измеримо тогда и только тогда, когда s и t измеримы по отдельно взятым сигма-алгебрам.
LaTeX
$$$(s \times t) \neq \emptyset \rightarrow \bigl( \operatorname{MeasurableSet}(s \times t) \iff ( \operatorname{MeasurableSet}(s) \land \operatorname{MeasurableSet}(t) ) \bigr)$$$
Lean4
theorem measurableSet_prod_of_nonempty {s : Set α} {t : Set β} (h : (s ×ˢ t).Nonempty) :
MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t :=
by
rcases h with ⟨⟨x, y⟩, hx, hy⟩
refine ⟨fun hst => ?_, fun h => h.1.prod h.2⟩
have : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t) := measurable_prodMk_right hst
have : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t) := measurable_prodMk_left hst
simp_all
