English
Let P be a projective family of measures. If a measurable cylinder s equals cylinder I S for some finite index set I and measurable S, then the value of the projective family on s coincides with the corresponding finite-dimensional measure P I S.
Русский
Пусть P -- проектная семейство мер. Если измеримое цилиндрическое множество s равно цилиндру I S для некоторого конечного множества индексов I и измеримого множества S, то значение проектной семейной меры на s равно сколь угодно соответствующей конечной мерe P I S.
LaTeX
$$$\forall hP\, hs\, hs\_eq\, hS:\ IsProjectiveMeasureFamily\ P \wedge s\in measurableCylinders\alpha \wedge s = cylinder I S \wedge S\ MeasurableSet\Rightarrow\ projectiveFamilyFun\ P\ s = P I S$$$
Lean4
theorem projectiveFamilyFun_congr (hP : IsProjectiveMeasureFamily P) (hs : s ∈ measurableCylinders α)
(hs_eq : s = cylinder I S) (hS : MeasurableSet S) : projectiveFamilyFun P s = P I S :=
by
rw [projectiveFamilyFun, dif_pos hs]
exact
hP.congr_cylinder (measurableCylinders.measurableSet hs) hS ((measurableCylinders.eq_cylinder hs).symm.trans hs_eq)
