monotone_of_nonneg — Mathlib

English

If Λ is a linear functional defined on real-valued compactly supported functions and Λ is nonnegative on nonnegative inputs, then Λ is monotone: f ≤ g implies Λ(f) ≤ Λ(g).

Русский

Если Λ — линейный функционал на вещественных функциях с компактной поддержкой и Λ(f) ≥ 0 для всех f ≥ 0, то Λ монотонен: f ≤ g ⇒ Λ(f) ≤ Λ(g).

LaTeX

$$$\\text{If } Λ: C_c(X,\\mathbb{R})\\to\\mathbb{R} \\text{ is positive, then } f\\le g \\Rightarrow Λ(f)\\le Λ(g).$$$

Lean4

/-- The positivity of a linear functional `Λ` implies that `Λ` is monotone. -/
@[deprecated PositiveLinearMap.mk₀ (since := "2025-08-08")]
theorem monotone_of_nonneg {Λ : C_c(X, ℝ) →ₗ[ℝ] ℝ} (hΛ : ∀ f, 0 ≤ f → 0 ≤ Λ f) : Monotone Λ :=
  (PositiveLinearMap.mk₀ Λ hΛ).monotone

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