toNNReal_mul_add_neg_mul_add_mul_neg_eq

English

For f,g in C(X, ℝ)₀, a certain NNReal identity holds relating (f·g) and sums of products with negations, expressing a distributive-like balance after applying toNNReal.

Русский

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

LaTeX

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

Lean4

theorem toNNReal_mul_add_neg_mul_add_mul_neg_eq (f g : C(X, ℝ)₀) :
    ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) =
      ((-(f * g)).toNNReal + f.toNNReal * 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_mul_add_neg_mul_add_mul_neg_eq g

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