iSup_partitionFiltration_eq_generateFrom_range

English

The iSup of the partition filtration levels equals the sigma-algebra generated by the range of t.

Русский

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

LaTeX

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

Lean4

theorem iSup_partitionFiltration_eq_generateFrom_range (ht : ∀ n, MeasurableSet (t n)) :
    ⨆ n, partitionFiltration ht n = generateFrom (Set.range t) :=
  by
  conv_rhs => rw [← generateFrom_iUnion_memPartition t, ← iSup_generateFrom]
  rfl

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