instCoeFunFiltrationForallMeasurableSpace

English

There is a canonical coercion from filtrations to indexable families of measurable spaces: f i = f.seq i.

Русский

Существует каноническое приведение фильтрации к семейству пространств с измеримыми сигм-алгебрами: f i = seq i.

LaTeX

$$$[\\text{instance}]\\; \\mathrm{CoeeFunFiltrationForallMeasurableSpace} \\Rightarrow \\forall i, f.seq i = \\cdot$$$

Lean4

instance [Preorder ι] : CoeFun (Filtration ι m) fun _ => ι → MeasurableSpace Ω :=
  ⟨fun f => f.seq⟩

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