lt_one_of_lt_one

Mathlib.Analysis.SpecialFunctions.SmoothTransition

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

← MathLib Explorer

English

If x < 1, then smoothTransition(x) < 1.

Русский

Если x < 1, тогда smoothTransition(x) < 1.

LaTeX

$$$$ x < 1 \implies \operatorname{smoothTransition}(x) < 1. $$$$

Lean4

theorem lt_one_of_lt_one (h : x < 1) : smoothTransition x < 1 :=
  (div_lt_one <| pos_denom x).2 <| lt_add_of_pos_right _ <| pos_of_pos <| sub_pos.2 h

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

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

Разделы

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

Аффилиация

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