min — Mathlib

English

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

Русский

Если две функции сходятся к пределам a1, a2 и сшиваются через min, получающийся предел равен min(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. \min(f(b),g(b)))\ b\ (\mathcal{nhds}\min(a_1,a_2)).$$$

Lean4

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

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