measurableCylinders — Mathlib

English

The collection of all cylinders with measurable base is the union over finite index sets and measurable bases.

Русский

Множество всех цилиндров с измеримыми основаниями — это объединение по конечным множествам индексов и измеримым основаниям.

LaTeX

$$$ \\mathrm{measurableCylinders}(\\alpha) \;=\; \\bigcup_{s} \\bigcup_{S} \\{\\mathrm{cylinder}(s,S) \\mid \\mathrm{MeasurableSet}(S)\\}$$$

Lean4

/-- Given a finite set `s` of indices, a cylinder is the preimage of a set `S` of `∀ i : s, α i` by
the projection from `∀ i, α i` to `∀ i : s, α i`.
`measurableCylinders` is the set of all cylinders with measurable base `S`. -/
def measurableCylinders (α : ι → Type*) [∀ i, MeasurableSpace (α i)] : Set (Set (∀ i, α i)) :=
  ⋃ (s) (S) (_ : MeasurableSet S), {cylinder s S}

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