mapHom — Mathlib

English

Push-forward defines a linear map: mapHom f is a linear map FiniteMeasure Ω → FiniteMeasure Ω'.

Русский

Пересылка определяет линейное отображение между множествами мер.

LaTeX

$$mapHom : FiniteMeasure Ω →ₗ[ℝ≥0] FiniteMeasure Ω' with toFun ν ↦ ν.map f$$

Lean4

/-- The push-forward of a finite measure by a function between measurable spaces as a linear map. -/
noncomputable def mapHom {f : Ω → Ω'} (f_mble : Measurable f) : FiniteMeasure Ω →ₗ[ℝ≥0] FiniteMeasure Ω'
    where
  toFun := fun ν ↦ ν.map f
  map_add' := map_add f_mble
  map_smul' := map_smul

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