English
MapRange respects linear structure with a linear map, as formalized via mapRangeₗ: applying a continuous linear map f to a vector measure v yields a linear map.
Русский
MapRange сохраняет линейную структуру через линейное отображение, задаваемое v и f.
LaTeX
$$$$ \\text{mapRange}\\_{\\ell}(f,hf)(v) = v.\\mathrm{mapRange}\\ f\\ hf. $$$$
Lean4
/-- Given a vector measure `v` on `M` and a continuous `AddMonoidHom` `f : M → N`, `f ∘ v` is a
vector measure on `N`. -/
def mapRange (v : VectorMeasure α M) (f : M →+ N) (hf : Continuous f) : VectorMeasure α N
where
measureOf' s := f (v s)
empty' := by rw [empty, AddMonoidHom.map_zero]
not_measurable' i hi := by rw [not_measurable v hi, AddMonoidHom.map_zero]
m_iUnion' _ hg₁ hg₂ := HasSum.map (v.m_iUnion hg₁ hg₂) f hf
