instSub

Mathlib.Topology.ContinuousMap.CompactlySupported

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

← MathLib Explorer

English

If f is nonnegative, then the nnrealPart of -f is identically zero.

Русский

Если f неотрицательно, то nnrealPart(-f) тождественно равна нулю.

LaTeX

$$$(-f).nnrealPart = 0$$$

Lean4

instance : Sub C_c(α, β) where
  sub f
    g :=
    { toFun := f.1 - g.1
      continuous_toFun := map_continuous (f.1 - g.1)
      hasCompactSupport' := by simpa [sub_eq_add_neg] using HasCompactSupport.add f.2 (-g).2 }

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

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

Разделы

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

Аффилиация

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