nnrealPart_add_le_add_nnrealPart — Mathlib

English

For compactly supported real-valued functions f and g, the nnrealPart of their sum does not exceed the sum of their nnrealParts: (f + g).nnrealPart ≤ f.nnrealPart + g.nnrealPart.

Русский

Для компактно поддерживаемых вещественных функций f и g выполнено неравенство: (f+g).nnrealPart ≤ f.nnrealPart + g.nnrealPart.

LaTeX

$$$ (f + g)^{\\mathrm{nnrealPart}} \\le f^{\\mathrm{nnrealPart}} + g^{\\mathrm{nnrealPart}}. $$$

Lean4

theorem nnrealPart_add_le_add_nnrealPart (f g : C_c(α, ℝ)) : (f + g).nnrealPart ≤ f.nnrealPart + g.nnrealPart :=
  by
  intro x
  simpa using Real.toNNReal_add_le

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