measurableSet_memPartitionSet — Mathlib

English

In the countably generated setting, memPartitionSet t n a is measurable for all a and n given t n are measurable.

Русский

В условиях счётного порождения, множество memPartitionSet t n a измеримо для всех a и n при условии, что t n измеримы.

LaTeX

$$$\forall n, \forall a,\MeasurableSet(memPartitionSet(t,n,a))$$$

Lean4

theorem measurableSet_memPartitionSet [MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ n, MeasurableSet (t n)) (n : ℕ)
    (a : α) : MeasurableSet (memPartitionSet t n a) :=
  measurableSet_memPartition ht n (memPartitionSet_mem t n a)

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