English
SupSet construction for filtrations redefines the i-th level as the supremum of all i-th levels in the set; it equips Filtration with an order‑theoretic supremum over a family.
Русский
Конструкция SupSet для филтраций задаёт i‑й уровень как наивысшее (супремум) среди i‑й уровней членов множества, образуя фильтрацию как семейство над порядком.
LaTeX
$$$\\mathrm{instSupSet}.seq i = \\mathsf{sSup}\\{ f(i) : f \\in s \\}$$$
Lean4
/-- Given a sequence of measurable sets `(sₙ)`, `filtrationOfSet` is the smallest filtration
such that `sₙ` is measurable with respect to the `n`-th sub-σ-algebra in `filtrationOfSet`. -/
def filtrationOfSet {s : ι → Set Ω} (hsm : ∀ i, MeasurableSet (s i)) : Filtration ι m
where
seq i := MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}
mono' _ _ hnm := MeasurableSpace.generateFrom_mono fun _ ⟨k, hk₁, hk₂⟩ => ⟨k, hk₁.trans hnm, hk₂⟩
le' _ := MeasurableSpace.generateFrom_le fun _ ⟨k, _, hk₂⟩ => hk₂ ▸ hsm k
