const — Mathlib

English

The constant filtration assigns the same σ-algebra m' to every index i, with monotonicity given by the constant map.

Русский

Постоянная фильтрация назначает на каждый индекс одно и то же σ-алгебру m'.

LaTeX

$$$\\mathrm{Filtration.const}(m',hm')$$$

Lean4

/-- The constant filtration which is equal to `m` for all `i : ι`. -/
def const (m' : MeasurableSpace Ω) (hm' : m' ≤ m) : Filtration ι m :=
  ⟨fun _ => m', monotone_const, fun _ => hm'⟩

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