eventually_one_sub_smoothingFn_nonneg

English

The map x ↦ ε(x) is strictly decreasing on (1, ∞); consequently, x ↦ 1 − ε(x) is strictly increasing on (1, ∞).

Русский

Отображение x ↦ ε(x) строго убывает на (1, ∞); следовательно, x ↦ 1 − ε(x) строго возрастает на (1, ∞).

LaTeX

$$$$\text{on }(1,\infty):\; \varepsilon(x)\text{ strictly decreases, hence } x \mapsto 1-\varepsilon(x)\text{ strictly increases.}$$$$

Lean4

theorem eventually_one_sub_smoothingFn_nonneg : ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 - ε n := by
  filter_upwards [eventually_one_sub_smoothingFn_pos] with n hn; exact le_of_lt hn

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