eventually_lt — Mathlib

English

If f and g are continuous at x0 and f(x0) < g(x0), then f < g holds in some neighborhood of x0.

Русский

Если функции f и g непрерывны в точке x0 и f(x0) < g(x0), то в некоторой окрестности x0 выполняется f(x) < g(x).

LaTeX

$$$\forall {x_0},\; (\text{ContinuousAt } f\ x_0) \land (\text{ContinuousAt } g\ x_0) \land f(x_0) < g(x_0) \Rightarrow \forall^\infty x \in \mathcal{N} x_0,\ f(x) < g(x).$$$

Lean4

nonrec theorem eventually_lt {x₀ : β} (hf : ContinuousAt f x₀) (hg : ContinuousAt g x₀) (hfg : f x₀ < g x₀) :
    ∀ᶠ x in 𝓝 x₀, f x < g x :=
  hf.eventually_lt hg hfg

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