projectiveFamilyContent_congr — Mathlib

English

For any measurable cylinder representation s = cylinder I S, the content equals the finite-dimensional measure: projectiveFamilyContent hP s = P I S.

Русский

Для любого представления цилиндра s = cylinder I S контент равен конечномерной мере: projectiveFamilyContent hP s = P I S.

LaTeX

$$$\operatorname{projectiveFamilyContent} hP s = P I S \quad \text{whenever } s = \operatorname{cylinder} I S \text{ and } S \text{ is measurable}$$$

Lean4

theorem projectiveFamilyContent_congr (hP : IsProjectiveMeasureFamily P) (s : Set (Π i, α i)) (hs_eq : s = cylinder I S)
    (hS : MeasurableSet S) : projectiveFamilyContent hP s = P I S := by
  rw [projectiveFamilyContent_eq,
    projectiveFamilyFun_congr hP ((mem_measurableCylinders s).mpr ⟨I, S, hS, hs_eq⟩) hs_eq hS]

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