neg_mulExpNegMulSq_neg — Mathlib

English

For every ε, x ∈ ℝ, mulExpNegMulSq ε x is an odd function of x; equivalently mulExpNegMulSq ε (−x) = − mulExpNegMulSq ε x.

Русский

Для любых ε, x ∈ ℝ функция mulExpNegMulSq ε x нечетна по переменной x; то есть mulExpNegMulSq ε (−x) = − mulExpNegMulSq ε x.

LaTeX

$$$\\forall \\varepsilon \\in \\mathbb{R}, \\forall x \\in \\mathbb{R},\\; mulExpNegMulSq\\,\\varepsilon\\,(-x) = -\\,mulExpNegMulSq\\,\\varepsilon\\,x$$$

Lean4

theorem neg_mulExpNegMulSq_neg (ε x : ℝ) : -mulExpNegMulSq ε (-x) = mulExpNegMulSq ε x := by simp [mulExpNegMulSq]

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