measurableSet_generateFrom_countablePartition_iff

English

For α with a countably generated measurable space and any natural n, a set s is measurable with respect to generateFrom (countablePartition α n) if and only if s is a finite union of blocks from countablePartition α n.

Русский

Пусть α имеет счетно генерируемое измеримое пространство. Множество s измеримо относительно generateFrom(countablePartition α n) тогда и только тогда, когда s является конечным объединением блоков countablePartition α n.

LaTeX

$$$$ MeasurableSet[generateFrom\\,(countablePartition\\,\\alpha\\,n)]\\,s \\iff \\exists S :\\ Finset (Set \\alpha), \\uparrow S \\subseteq countablePartition\\,\\alpha\\,n \\wedge s = \\bigcup_{A\\in S} A. $$$$

Lean4

theorem measurableSet_generateFrom_countablePartition_iff (n : ℕ) (s : Set α) :
    MeasurableSet[generateFrom (countablePartition α n)] s ↔
      ∃ S : Finset (Set α), ↑S ⊆ countablePartition α n ∧ s = ⋃₀ S :=
  measurableSet_generateFrom_memPartition_iff _ n s

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