eq_toRealPositiveLinear_toReal — Mathlib

English

The evaluation formula for toRealPositiveLinear Λ on f is the same as in the previous entry: toRealPositiveLinear Λ (f) = Λ (nnrealPart f) - Λ (nnrealPart (-f)).

Русский

Формула применения toRealPositiveLinear Λ к f повторяет предыдущее: toRealPositiveLinear Λ (f) = Λ (nnrealPart f) - Λ (nnrealPart (-f)).

LaTeX

$$$ toRealPositiveLinear(Λ)(f) = Λ(\mathrm{nnrealPart}(f)) - Λ(\mathrm{nnrealPart}(-f)) $$$

Lean4

@[simp]
theorem eq_toRealPositiveLinear_toReal (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) (f : C_c(α, ℝ≥0)) :
    toRealPositiveLinear Λ (toReal f) = Λ f := by simp [toRealPositiveLinear_apply]

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