measurableSet_prod — Mathlib

English

Let s ⊆ α and t ⊆ β. Then MeasurableSet(s × t) holds iff either both s and t are measurable or one of them is empty.

Русский

Пусть s ⊆ α и t ⊆ β. Множество s × t измеримо тогда и только тогда, когда либо оба множества измеримы, либо одно из них пусто.

LaTeX

$$$\operatorname{MeasurableSet}(s \times t) \iff (\operatorname{MeasurableSet}(s) \land \operatorname{MeasurableSet}(t)) \lor s = \emptyset \lor t = \emptyset$$$

Lean4

theorem measurableSet_prod {s : Set α} {t : Set β} :
    MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅ :=
  by
  rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
  · simp [h, prod_eq_empty_iff.mp h]
  · simp [← not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, measurableSet_prod_of_nonempty h]

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