abs_mulExpNegMulSq_one_le_one

Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

URI: https://scilib.ai/kg/mathlib#Real.abs_mulExpNegMulSq_one_le_one

← MathLib Explorer

English

For all x ∈ ℝ, |mulExpNegMulSq 1 x| ≤ 1.

Русский

Для всех x ∈ ℝ выполняется |mulExpNegMulSq 1 x| ≤ 1.

LaTeX

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

Lean4

theorem abs_mulExpNegMulSq_one_le_one (x : ℝ) : |mulExpNegMulSq 1 x| ≤ 1 :=
  abs_le.mpr ⟨neg_one_le_mulExpNegMulSq_one x, mulExpNegMulSq_one_le_one x⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru