toNNReal_mul_add_neg_mul_add_mul_neg_eq

English

A pointwise identity for NNReal-valued products and mixes with negation: (f*g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal = (-(f*g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal.

Русский

Точечное тождество NNReal для произведения и смешения с отрицанием: (f*g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal = (-(f*g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal.

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
  ext x
  simp [max_neg_zero, add_mul, mul_add]
  abel

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