tendsto_nhds_min_right — Mathlib

English

Dual to max_right, for nhds within a right neighborhood.

Русский

Дуал к max_right, для nhds внутри правой окрестности.

LaTeX

$$$\text{Tendsto } f\ l\ (\mathcal{nhds[<]} a) \Rightarrow \text{Tendsto}(\lambda i. \min(a, f(i)))\ l\ (\mathcal{nhds[<]} a).$$$

Lean4

theorem tendsto_nhds_min_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝[<] a)) :
    Tendsto (fun i => min a (f i)) l (𝓝[<] a) :=
  Filter.tendsto_nhds_max_right (α := αᵒᵈ) h

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