le_of_tendsto_of_tendsto' — Mathlib

English

If f → a1 and g → a2 along b, and f x ≤ g x for all x, then a1 ≤ a2.

Русский

Если f сходится к a1 и g к a2 вдоль b, и ∀x, f(x) ≤ g(x), то a1 ≤ a2.

LaTeX

$$$\text{Tendsto } f b (\mathcal{N} a_1) \land \text{Tendsto } g b (\mathcal{N} a_2) \land \forall x, f(x) \le g(x) \Rightarrow a_1 \le a_2$$$

Lean4

theorem le_of_tendsto_of_tendsto' {f g : β → α} {b : Filter β} {a₁ a₂ : α} [NeBot b] (hf : Tendsto f b (𝓝 a₁))
    (hg : Tendsto g b (𝓝 a₂)) (h : ∀ x, f x ≤ g x) : a₁ ≤ a₂ :=
  le_of_tendsto_of_tendsto hf hg (Eventually.of_forall h)

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