nnrealPart_sub_nnrealPart_neg

Mathlib.Topology.ContinuousMap.CompactlySupported

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

English

The equality of the coercion of toRealLinearMap with toReal holds (simp).

Русский

Справедливо равенство отображения coe_toRealLinearMap: toRealLinearMap = toReal.

LaTeX

$$$toRealLinearMap = toReal$$$

Lean4

@[simp]
theorem nnrealPart_sub_nnrealPart_neg (f : C_c(α, ℝ)) : (nnrealPart f).toReal - (nnrealPart (-f)).toReal = f := by
  ext x; simp

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

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

Разделы

Аффилиация

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