toNNReal_add_add_neg_add_neg_eq — Mathlib

English

For f,g in C(X, ℝ)₀, the NNReal image of their sum with negations satisfies a balanced equality with the negation of their sum.

Русский

Для f,g в C(X, ℝ)₀ тождество для суммы с отрицаниями в NNReal равенству.

LaTeX

$$((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) = ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal)$$

Lean4

theorem toNNReal_add_add_neg_add_neg_eq (f g : C(X, ℝ)₀) :
    ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) = ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) :=
  by
  apply toContinuousMap_injective
  simpa only [← toContinuousMapHom_apply, map_add, map_mul, map_neg, toContinuousMapHom_toNNReal] using
    (f : C(X, ℝ)).toNNReal_add_add_neg_add_neg_eq g

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