integral_fun_snd — Mathlib

English

For f: β → E, ∫ z f(z.2) dμ×ν equals μ.real univ times ∫ f dy.

Русский

Для f: β → E интеграл по произведению μ×ν от f(z.2) равен μ.real univ умножить на интеграл по ν от f.

LaTeX

$$$$\\int z, f(z.2) \\, d(μ×ν) = (μ.real\\; univ) \\cdot \\int y, f(y) \\, dν.$$$$

Lean4

theorem integral_fun_snd (f : β → E) : ∫ z, f z.2 ∂μ.prod ν = μ.real univ • ∫ y, f y ∂ν := by
  simpa using integral_prod_smul (1 : α → ℝ) f

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