tendsto_nhds_max_right — Mathlib

English

If f l → a in nhds a, then max(a, f(i)) → a in nhds a.

Русский

Если f(l) сходится к a в окрестности a, то max(a, f(i)) сходится к a в nhds a.

LaTeX

$$$\text{Tendsto } f\ l\ (\mathcal{nhds} a) \Rightarrow \text{Tendsto}(\lambda i. \max(a, f(i)))\ l\ (\mathcal{nhds} a).$$$

Lean4

theorem tendsto_nhds_max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) :
    Tendsto (fun i => max a (f i)) l (𝓝[>] a) :=
  by
  obtain ⟨h₁ : Tendsto f l (𝓝 a), h₂ : ∀ᶠ i in l, f i ∈ Ioi a⟩ := tendsto_nhdsWithin_iff.mp h
  exact tendsto_nhdsWithin_iff.mpr ⟨h₁.max_right, h₂.mono fun i hi => lt_max_of_lt_right hi⟩

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