measurableSet_countablePartitionSet

English

Let α be a type with a measurable space structure that is countably generated. Then for any natural number n and any a ∈ α, the set countablePartitionSet n a is measurable.

Русский

Пусть α обладает структурой пространства измерения, порожденной счетно. Тогда для любого n ∈ ℕ и для любого a ∈ α множество countablePartitionSet n a измеримо.

LaTeX

$$$\forall n : \mathbb{N}, \forall a : \alpha,\ a \,\mapsto\ a \\in \\text{countablePartitionSet } n a \\text{ is measurable}$$$

Lean4

@[measurability]
theorem measurableSet_countablePartitionSet (n : ℕ) (a : α) : MeasurableSet (countablePartitionSet n a) :=
  measurableSet_countablePartition n (countablePartitionSet_mem n a)

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