IicSnd_apply — Mathlib

English

For any measurable s, IicSnd r applied to s equals ρ(s × Iic r).

Русский

Для любого измеримого множества s, IicSnd r(evaluated on s) равно ρ(s × Iic r).

LaTeX

$$$\rho.IicSnd(r)(s) = \rho\left(s \times Iic(r)\right)$$$

Lean4

theorem IicSnd_apply (r : ℝ) {s : Set α} (hs : MeasurableSet s) : ρ.IicSnd r s = ρ (s ×ˢ Iic r) := by
  rw [IicSnd, fst_apply hs, restrict_apply' (MeasurableSet.univ.prod measurableSet_Iic), univ_prod, Set.prod_eq]

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