of_mem_measurableCylinders — Mathlib

English

If t is a measurable cylinder, then t equals cylinder of its finite index set and its base set.

Русский

Если t — измеримый цилиндр, то t равен цилиндру, заданному его конечным множеством индексов и основанием.

LaTeX

$$$ t = \\mathrm{cylinder}(\\mathrm{measurableCylinders.finset}(t), \\mathrm{measurableCylinders.set}(t)) $$$

Lean4

@[measurability]
theorem _root_.MeasurableSet.of_mem_measurableCylinders {s : Set (Π i, α i)} (hs : s ∈ measurableCylinders α) :
    MeasurableSet s := by
  obtain ⟨I, t, mt, rfl⟩ := (mem_measurableCylinders s).1 hs
  exact mt.cylinder

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