le_of_tendsto_of_tendsto — Mathlib

English

If f → a1 and g → a2 along b, and f ≤ᶠ[b] g, then a1 ≤ a2.

Русский

Если f сходится к a1 и g к a2 вдоль b и f ≤ᶠ[b] g, то a1 ≤ a2.

LaTeX

$$$\text{Tendsto } f b (\mathcal{N} a_1) \land \text{Tendsto } g b (\mathcal{N} a_2) \land f \le^b g \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 : f ≤ᶠ[b] g) : a₁ ≤ a₂ :=
  le_of_tendsto_of_tendsto_of_frequently hf hg <| Eventually.frequently h

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