iSup_partitionFiltration — Mathlib

English

For ht, the supremum over n of partitionFiltration ht n equals generateFrom(range t).

Русский

Для ht верхняя грань по n фильтрации partitionFiltration ht n равна generateFrom(range t).

LaTeX

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

Lean4

theorem iSup_partitionFiltration (ht : ∀ n, MeasurableSet (t n)) (ht_range : generateFrom (Set.range t) = m) :
    ⨆ n, partitionFiltration ht n = m := by rw [iSup_partitionFiltration_eq_generateFrom_range ht, ht_range]

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