coeAddHom — Mathlib

English

For any measure μ, the map coeAddHom(μ) equals μ itself as a function: coeAddHom μ = ⇑μ.

Русский

Для меры μ отображение coeAddHom(μ) совпадает с μ как функцией: coeAddHom μ = ⇑μ.

LaTeX

$$$\text{coeAddHom }\mu = \nolinebreak[4] ⇑\mu$$$

Lean4

/-- Coercion to function as an additive monoid homomorphism. -/
def coeAddHom {_ : MeasurableSpace α} : Measure α →+ Set α → ℝ≥0∞
    where
  toFun := (⇑)
  map_zero' := coe_zero
  map_add' := coe_add

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