projectiveFamilyContent_cylinder — Mathlib

English

If S is measurable, then the content of cylinder I S equals P I S.

Русский

Если S измеримо, то содержание цилиндра I S равно P I S.

LaTeX

$$$\text{MeasurableSet } S \Rightarrow \operatorname{projectiveFamilyContent} hP (\operatorname{cylinder} I S) = P I S$$$

Lean4

theorem projectiveFamilyContent_cylinder (hP : IsProjectiveMeasureFamily P) (hS : MeasurableSet S) :
    projectiveFamilyContent hP (cylinder I S) = P I S :=
  projectiveFamilyContent_congr _ _ rfl hS

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