sigmaFiniteFiltration — Mathlib

English

If μ is finite and f is a filtration, then the same sigma-finite property holds across all indices i for μ.trim(f.le i).

Русский

Если μ конечна и есть фильтрация f, то свойство сигма‑финитности сохраняется на каждом уровне i для μ.trim(f.le i).

LaTeX

$$$[IsFiniteMeasure μ] \\Rightarrow [\\text{SigmaFiniteFiltration } μ f] \\Rightarrow \\forall i, \\ SigmaFinite (\\mu.trim (f.le i)).$$$

Lean4

instance (priority := 100) sigmaFiniteFiltration [Preorder ι] (μ : Measure Ω) (f : Filtration ι m) [IsFiniteMeasure μ] :
    SigmaFiniteFiltration μ f :=
  ⟨fun n => by infer_instance⟩

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