toReal_nonneg

Mathlib.Topology.ContinuousMap.CompactlySupported

URI: https://scilib.ai/kg/mathlib#CompactlySupportedContinuousMap.toReal_nonneg

English

If f is a nonnegative-valued compactly supported function, then its real realization is nonnegative.

Русский

Если f принимает неотрицательные значения и имеет компактную поддержку, то f.toReal неотрицательно.

LaTeX

$$$ 0 \\le f^{\\mathrm{toReal}}. $$$

Lean4

@[simp]
theorem toReal_nonneg {f : C_c(α, ℝ≥0)} : 0 ≤ f.toReal := fun _ ↦ by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru