le_one

Mathlib.Analysis.SpecialFunctions.SmoothTransition

URI: https://scilib.ai/kg/mathlib#Real.smoothTransition.le_one

English

For all real x, smoothTransition(x) ≤ 1.

Русский

Для любого x из ℝ, smoothTransition(x) ≤ 1.

LaTeX

$$$$ \forall x \in \mathbb{R},\ \operatorname{smoothTransition}(x) \le 1. $$$$

Lean4

theorem le_one (x : ℝ) : smoothTransition x ≤ 1 :=
  (div_le_one (pos_denom x)).2 <| le_add_of_nonneg_right (nonneg _)

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

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

Разделы

Аффилиация

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