English
The content associated to a cylinder-based measurable cylinder coincides with the corresponding projective function: projectiveFamilyContent hP s = projectiveFamilyFun P s for any s.
Русский
Контент, связанный с цилиндрическим множеством, совпадает с соответствующей функцией проектной семейной меры: projectiveFamilyContent hP s = projectiveFamilyFun P s для любого s.
LaTeX
$$$\operatorname{projectiveFamilyContent} hP s = \operatorname{projectiveFamilyFun} P s$$$
Lean4
/-- For `P` a projective family of measures, we define an additive content on the measurable
cylinders, by setting `projectiveFamilyContent s = P I S` for `s = cylinder I S`, where `I` is
a finite set of indices and `S` is a measurable set in `Π i : I, α i`. -/
noncomputable def projectiveFamilyContent (hP : IsProjectiveMeasureFamily P) : AddContent (measurableCylinders α) :=
isSetRing_measurableCylinders.addContent_of_union (projectiveFamilyFun P) (projectiveFamilyFun_empty hP)
(projectiveFamilyFun_union hP)
