English
Consider finite-coordinate cylinder events on a product space Ω^α. The exterior σ-algebras of finite subsets of α form a cofiltration indexed by Finset α, where the level corresponding to Λ ⊆ α is generated by cylinder sets that depend on coordinates outside Λ, yielding a decreasing family with respect to inclusion.
Русский
Рассматривая цилиндрические множества на произведении Ω^α, внешние сигма-алгебры по конечным подмножествам α образуют кофильтрацию, индексируемую Finset α: уровень, соответствующий Λ ⊆ α, порождается цилиндрическими множествами, зависящими от координат вне Λ; это даёт нисходящую по включению семью.
LaTeX
$$$\{ \mathcal{F}_{\Lambda} : \Lambda \subseteq_f \alpha\} \text{ с обратным порядком } \subseteq, \\ \mathcal{F}_{\Lambda} = \sigma\bigl(\text{cylinder sets depending on } \alpha\setminus \Lambda\bigr).$$$
Lean4
/-- The exterior σ-algebras of finite sets of `α` form a cofiltration indexed by `Finset α`. -/
def cylinderEventsCompl : Filtration (Finset α)ᵒᵈ (.pi (X := fun _ : α ↦ Ω))
where
seq Λ := cylinderEvents (↑(OrderDual.ofDual Λ))ᶜ
mono' _ _ h := cylinderEvents_mono <| Set.compl_subset_compl_of_subset h
le' _ := cylinderEvents_le_pi
