tendsto_nhds_max_left — Mathlib

English

Symmetric to max_right, but with left-neighborhoods.

Русский

Симметрично к max_right, для левых окрестностей.

LaTeX

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

Lean4

theorem tendsto_nhds_max_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) :
    Tendsto (fun i => max (f i) a) l (𝓝[>] a) :=
  by
  simp_rw [max_comm _ a]
  exact Filter.tendsto_nhds_max_right h

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