pos_of_pos

Mathlib.Analysis.SpecialFunctions.SmoothTransition

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

English

The equality smoothTransition(x) = 1 holds exactly when 1 ≤ x.

Русский

Равенство smoothTransition(x) = 1 выполняется ровно тогда, когда 1 ≤ x.

LaTeX

$$$$ \operatorname{smoothTransition}(x) = 1 \iff 1 \le x. $$$$

Lean4

theorem pos_of_pos (h : 0 < x) : 0 < smoothTransition x :=
  div_pos (expNegInvGlue.pos_of_pos h) (pos_denom x)

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

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

Разделы

Аффилиация

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