eq_toNNRealLinear_toRealPositiveLinear

English

For any Λ, applying toRealPositiveLinear toReal f yields Λ f when f is already nonnegative: toRealPositiveLinear Λ (toReal f) = Λ f.

Русский

Для любого Λ применение toRealPositiveLinear к toReal f даёт Λ f, когда f неотрицательно.

LaTeX

$$$ toRealPositiveLinear Λ (toReal f) = Λ f $$$

Lean4

@[simp]
theorem eq_toNNRealLinear_toRealPositiveLinear (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) :
    toNNRealLinear (toRealPositiveLinear Λ) = Λ := by
  ext f
  simp

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