min_right

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#Filter.Tendsto.min_right

English

If f → a, then min(a, f(i)) → a.

Русский

Если f → a, тогда min(a, f(i)) → a.

LaTeX

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

Lean4

theorem min_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) : Tendsto (fun i => min a (f i)) l (𝓝 a) :=
  Filter.Tendsto.max_right (α := αᵒᵈ) h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru