measurableSet_memPartition — Mathlib

English

If every t(n) is measurable, then any s in memPartition t n is measurable.

Русский

Если каждый t(n) измерим, то любое s, принадлежащее memPartition t n, измеримо.

LaTeX

$$$\forall n, \forall s\ (s \in memPartition(t,n)\Rightarrow \MeasurableSet(s))$$$

Lean4

theorem measurableSet_memPartition [MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ n, MeasurableSet (t n)) (n : ℕ)
    {s : Set α} (hs : s ∈ memPartition t n) : MeasurableSet s :=
  generateFrom_memPartition_le ht n _ (measurableSet_generateFrom hs)

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