toRealLinearMap — Mathlib

English

For f : C_c(α, ℝ), if f ≥ 0, then (nnrealPart f).toReal - (nnrealPart(-f)).toReal = f.

Русский

Для f : C_c(α, ℝ), если f ≥ 0, то (nnrealPart f).toReal - (nnrealPart(-f)).toReal = f.

LaTeX

$$$(nnrealPart\, f).toReal - (nnrealPart(-f)).toReal = f$$$

Lean4

/-- The map `toReal` defined as a `ℝ≥0`-linear map. -/
noncomputable def toRealLinearMap : C_c(α, ℝ≥0) →ₗ[ℝ≥0] C_c(α, ℝ)
    where
  toFun := toReal
  map_add' f g := by ext x; simp
  map_smul' a f := by ext x; simp

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