strictAntiOn_smoothingFn — Mathlib

English

The smoothing function ε is strictly decreasing on (1, ∞). Consequently, the map x ↦ (1 + ε(x)) is strictly decreasing on (1, ∞).

Русский

Функция сглаживания ε строго убывает на (1, ∞). Следовательно, отображение x ↦ 1 + ε(x) строго убывает на (1, ∞).

LaTeX

$$$$\text{StrictAntiOn}(\varepsilon, (1,\infty))\quad\text{and}\quad \text{StrictAntiOn}(1+\varepsilon(x), (1,\infty)).$$$$

Lean4

theorem strictAntiOn_smoothingFn : StrictAntiOn ε (Set.Ioi 1) :=
  by
  change StrictAntiOn (fun x => 1 / log x) (Set.Ioi 1)
  simp_rw [one_div]
  refine StrictAntiOn.comp_strictMonoOn inv_strictAntiOn ?log fun _ hx => log_pos hx
  refine StrictMonoOn.mono strictMonoOn_log (fun x hx => ?_)
  exact Set.Ioi_subset_Ioi zero_le_one hx

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