max_right — Mathlib

English

If f tends to a along l, then max(a,f(i)) tends to a along l.

Русский

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

LaTeX

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

Lean4

protected theorem max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) : Tendsto (fun i => max a (f i)) l (𝓝 a) :=
  by simpa only [sup_idem] using (tendsto_const_nhds (x := a)).max h

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