neg_one_le_mulExpNegMulSq_one — Mathlib

English

For every x ∈ ℝ, mulExpNegMulSq 1 x ≥ −1 (since the function is nonnegative, this bound is trivial).

Русский

Для каждого x ∈ ℝ выполняется mulExpNegMulSq 1 x ≥ −1 (функция неотрицательна, поэтому нестрогая граница тривиальна).

LaTeX

$$$\\forall x \\in \\mathbb{R},\\; -1 \\le mulExpNegMulSq(1, x)$$$

Lean4

theorem neg_one_le_mulExpNegMulSq_one (x : ℝ) : -1 ≤ mulExpNegMulSq 1 x :=
  by
  rw [← neg_mulExpNegMulSq_neg, neg_le_neg_iff]
  exact mulExpNegMulSq_one_le_one (-x)

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