measurableSet_succ_countablePartition

English

If s is a block of the n-th partition, then s is measurable with respect to the sigma-algebra generated by the (n+1)-st partition: s ∈ countablePartition α n ⇒ MeasurableSet[generateFrom (countablePartition α (n+1))] s.

Русский

Если s — блок разбиения n-й, то s измеримо относительно сигма-алгебры, порождаемой (n+1)-й разбиением: s ∈ countablePartition α n ⇒ MeasurableSet[generateFrom (countablePartition α (n+1))] s.

LaTeX

$$$$ s \\in countablePartition\\,\\alpha\\,n \\Rightarrow MeasurableSet\\[generateFrom\\,(countablePartition\\,\\alpha\\,(n+1))\\]\\,s. $$$$

Lean4

theorem measurableSet_succ_countablePartition (n : ℕ) {s : Set α} (hs : s ∈ countablePartition α n) :
    MeasurableSet[generateFrom (countablePartition α (n + 1))] s :=
  measurableSet_succ_memPartition _ _ hs

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