max — Mathlib

English

If two functions converge to limits a1, a2 and are combined via max, the resulting limit is max(a1,a2).

Русский

Если две функции сходятся к пределам a1, a2 и сшиваются через max, получающийся предел равен max(a1,a2).

LaTeX

$$$\text{Tendsto } f\ b\ (\mathcal{nhds}\ a_1) \land \text{Tendsto } g\ b\ (\mathcal{nhds}\ a_2) \Rightarrow \text{Tendsto } (\lambda b. \max(f(b),g(b)))\ b\ (\mathcal{nhds}\max(a_1,a_2)).$$$

Lean4

protected theorem max {b : Filter β} {a₁ a₂ : α} (hf : Tendsto f b (𝓝 a₁)) (hg : Tendsto g b (𝓝 a₂)) :
    Tendsto (fun b => max (f b) (g b)) b (𝓝 (max a₁ a₂)) :=
  (continuous_max.tendsto (a₁, a₂)).comp (hf.prodMk_nhds hg)

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