toRealLinear_nonneg

Mathlib.Topology.ContinuousMap.CompactlySupported

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

← MathLib Explorer

English

If g ∈ C_c(α, ℝ) with g ≥ 0, then 0 ≤ toRealPositiveLinear Λ g.

Русский

Если g ∈ C_c(α, ℝ) неотрицательно, то 0 ≤ toRealPositiveLinear Λ g.

LaTeX

$$$ 0 \le toRealPositiveLinear(\Lambda)\; g $$$

Lean4

@[deprecated map_nonneg (since := "2025-08-08")]
theorem toRealLinear_nonneg (Λ : C_c(α, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) (g : C_c(α, ℝ)) (hg : 0 ≤ g) : 0 ≤ toRealPositiveLinear Λ g :=
  map_nonneg _ hg

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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