le_of_tendsto_of_tendsto_of_frequently

English

If f and g converge to a1 and a2 respectively along b, and f ≤ g frequently, then a1 ≤ a2.

Русский

Если f и g сходятся к a1 и a2 соответственно вдоль b, и f ≤ g часто (frequently), то a1 ≤ a2.

LaTeX

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

Lean4

theorem le_of_tendsto_of_tendsto_of_frequently {f g : β → α} {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁))
    (hg : Tendsto g b (𝓝 a₂)) (h : ∃ᶠ x in b, f x ≤ g x) : a₁ ≤ a₂ :=
  t.isClosed_le'.mem_of_frequently_of_tendsto h (hf.prodMk_nhds hg)

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