measurableSet_pi — Mathlib

English

For a countable s, MeasurableSet(pi s t) holds iff either every t(i) is measurable for i ∈ s, or pi s t = ∅.

Русский

Для счётного множества s верно: MeasurableSet(pi s t) тогда и только тогда, когда либо все t(i) измеримы при i ∈ s, либо pi s t = ∅.

LaTeX

$$$\\text{MeasurableSet}(\\pi s t) \\iff (\\forall i \\in s, \\text{MeasurableSet}(t i)) \\lor (\\pi s t = \\emptyset)$$$

Lean4

theorem measurableSet_pi {s : Set δ} {t : ∀ i, Set (X i)} (hs : s.Countable) :
    MeasurableSet (pi s t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ pi s t = ∅ :=
  by
  rcases (pi s t).eq_empty_or_nonempty with h | h
  · simp [h]
  · simp [measurableSet_pi_of_nonempty hs, h, ← not_nonempty_iff_eq_empty]

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