generatePiSystem_measurableSet — Mathlib

English

If every member s of g is measurable, then any t in generatePiSystem(g) is measurable with respect to generateFrom g.

Русский

Если каждый элемент s из g измерим, то любой t из generatePiSystem(g) измерим в generateFrom g.

LaTeX

$$$$ \forall s \in g,\ MeasurableSet(s) \implies (t \in \mathrm{generatePiSystem}(g)\Rightarrow \ MeasurableSet_{generateFrom(g)}(t)) $$$$

Lean4

theorem generatePiSystem_measurableSet [M : MeasurableSpace α] {S : Set (Set α)} (h_meas_S : ∀ s ∈ S, MeasurableSet s)
    (t : Set α) (h_in_pi : t ∈ generatePiSystem S) : MeasurableSet t := by
  induction h_in_pi with
  | base h_s => apply h_meas_S _ h_s
  | inter _ _ _ h_s h_u => apply MeasurableSet.inter h_s h_u

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