measurable_memPartitionSet — Mathlib

English

The iSup (direct supremum) of the partition filtrations equals the sigma-algebra generated by the sets t(n).

Русский

Предел по iSup фильтраций разбиений равен сигма-алгебре, порождаемой множествами t(n).

LaTeX

$$$$ \bigvee_{n} \ partitionFiltration\; ht\; n = generateFrom(\operatorname{range} t) $$$$

Lean4

theorem measurable_memPartitionSet (ht : ∀ n, MeasurableSet (t n)) (n : ℕ) : Measurable (memPartitionSet t n) :=
  (measurable_partitionFiltration_memPartitionSet ht n).mono ((partitionFiltration ht).le n) le_rfl

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