ge_of_tendsto'

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#ge_of_tendsto'

English

If Tendsto f x (nhds a) and f ≥ b pointwise, then b ≤ a.

Русский

Если f сходится к a в nhds и для всех c выполняется b ≤ f c, то b ≤ a.

LaTeX

$$$ \text{Tendsto } f\ x\ (nhds a) \; \&\; (\forall c, b \le f c) \Rightarrow b \le a $$$

Lean4

theorem ge_of_tendsto' {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) (h : ∀ c, b ≤ f c) : b ≤ a :=
  ge_of_tendsto lim (Eventually.of_forall h)

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

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

Разделы

Аффилиация

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