English
For every finite set s, the filtration level piFinset(X, s) equals the comap of the product sigma-algebra under the restriction map to coordinates in s; i.e., the level is the same as pulling back the product σ-algebra along the projection to s.
Русский
Для каждого конечного множества s фильтрация на уровне piFinset(X, s) равна прообразу (comap) произведной сигма-алгебры при ограничении к координатам в s; то есть этот уровень совпадает с возвратом σ-алгебры через проекцию на координаты из s.
LaTeX
$$$\mathcal{F}_s = \pi\text{-comap}(s)\;\text{where } s:\ Finset(\mathcal{I})$, i.e. $\mathcal{F}_s = \pi_s^{-1}\bigl( \bigotimes_{i\in s} \mathcal{F}_i \bigr)$, with $\pi_s: \prod_{i\in\mathcal{I}} X_i \to \prod_{i\in s} X_i$ the coordinate projection.$$
Lean4
theorem piFinset_eq_comap_restrict (s : Finset ι) : piFinset (X := X) s = pi.comap s.toSet.restrict :=
rfl
