iSup_countableFiltration — Mathlib

English

The iSup over n of countableFiltration α n equals the measurable space m.

Русский

Область независимой нарастающей последовательности countableFiltration α n равна m.

LaTeX

$$$$ \bigvee_{n} countableFiltration α n = m $$$$

Lean4

theorem iSup_countableFiltration (α : Type*) [m : MeasurableSpace α] [CountablyGenerated α] :
    ⨆ n, countableFiltration α n = m :=
  by
  conv_rhs => rw [← generateFrom_iUnion_countablePartition α, ← iSup_generateFrom]
  rfl

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