monotone — Mathlib

English

The function smoothTransition is monotone on ℝ.

Русский

Функция smoothTransition монотонна на ℝ.

LaTeX

$$$$ \operatorname{Monotone}(\operatorname{smoothTransition}). $$$$

Lean4

protected theorem monotone : Monotone smoothTransition :=
  by
  intro x y hxy
  simp only [smoothTransition]
  rw [div_le_div_iff₀ (pos_denom x) (pos_denom y)]
  simp only [mul_add, mul_comm (expNegInvGlue x) (expNegInvGlue y), add_le_add_iff_left]
  gcongr
  · exact expNegInvGlue.nonneg _
  · exact expNegInvGlue.nonneg _
  · apply expNegInvGlue.monotone hxy
  · apply expNegInvGlue.monotone (by linarith)

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