monotone_of_nnreal — Mathlib

English

Let Λ be a linear functional on the space of compactly supported nonnegative real-valued continuous functions. Then Λ is order-preserving: if f ≤ g (pointwise), then Λ(f) ≤ Λ(g).

Русский

Пусть Λ — линейный функционал на пространстве компактно поддержанных неотрицательных непрерывных функций, принимающих значения в ℝ≥0. Тогда Λ сохраняет порядок: если f ≤ g по точкам, то Λ(f) ≤ Λ(g).

LaTeX

$$$\\text{If } f,g\\in C_c(X,\\mathbb{R}_{\\ge 0})\\text{ and } f\\le g,\\ \\text{then } \\Lambda f \\le \\Lambda g.$$$

Lean4

theorem monotone_of_nnreal : Monotone Λ := by
  intro f₁ f₂ h
  obtain ⟨g, hg⟩ := CompactlySupportedContinuousMap.exists_add_of_le h
  rw [← hg]
  simp

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