integral_map — Mathlib

English

The integral over a sum measure equals the infinite sum of the integrals: ∫ f d(∑ μ_i) = ∑' i, ∫ f dμ_i.

Русский

Интеграл по суммарной мере равен бесконечной сумме интегралов: ∫ f d(∑ μ_i) = ∑' i, ∫ f dμ_i.

LaTeX

$$$$\int a, f(a) \partial(\operatorname{sum} μ) = \sum' i, \int a, f(a) \partial μ_i.$$$$

Lean4

theorem _root_.Topology.IsClosedEmbedding.integral_map {β} [TopologicalSpace α] [BorelSpace α] [TopologicalSpace β]
    [MeasurableSpace β] [BorelSpace β] {φ : α → β} (hφ : IsClosedEmbedding φ) (f : β → G) :
    ∫ y, f y ∂Measure.map φ μ = ∫ x, f (φ x) ∂μ :=
  hφ.measurableEmbedding.integral_map _

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