max_left — Mathlib

English

Similarly to max_right, but with reverse order, max(f(i), a) tends to a when f(i) → a.

Русский

Аналогично max_right, max(f(i), a) сходится к a при f(i)→a.

LaTeX

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

Lean4

protected theorem 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 h.max_right

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