cylinder — Mathlib

English

If all α i carry a measurable space structure, then the cylinder of a measurable base is measurable.

Русский

Если у всех α i задана сигма-алгебра измеримости, цилиндр над измеримым основанием измерим.

LaTeX

$$$ \\mathrm{MeasurableSet}(S) \\Rightarrow \\mathrm{MeasurableSet}(\\mathrm{cylinder}(s,S)) $$$

Lean4

theorem _root_.MeasurableSet.cylinder [∀ i, MeasurableSpace (α i)] (s : Finset ι) {S : Set (∀ i : s, α i)}
    (hS : MeasurableSet S) : MeasurableSet (cylinder s S) :=
  measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS

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