integral_fun_fst — Mathlib

English

Symmetric statement to integral_fun_snd: ∫ z f z.fst dμ×ν equals ν.real univ times ∫ f dμ.

Русский

Симметричное утверждение к integral_fun_snd: интеграл по z f z.fst dμ×ν равен ν.real univ умножить на ∫ f dμ.

LaTeX

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

Lean4

theorem integral_fun_fst (f : α → E) : ∫ z, f z.1 ∂μ.prod ν = ν.real univ • ∫ x, f x ∂μ :=
  by
  rw [← integral_prod_swap]
  apply integral_fun_snd

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