one_of_one_le

Mathlib.Analysis.SpecialFunctions.SmoothTransition

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

← MathLib Explorer

English

Let x be a real number. If x ≥ 1, then smoothTransition(x) = 1.

Русский

Пусть x ∈ ℝ. При x ≥ 1 выполняется smoothTransition(x) = 1.

LaTeX

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

Lean4

theorem one_of_one_le (h : 1 ≤ x) : smoothTransition x = 1 :=
  (div_eq_one_iff_eq <| (pos_denom x).ne').2 <| by rw [zero_of_nonpos (sub_nonpos.2 h), add_zero]

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

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

Разделы

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

Аффилиация

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