eventually_ge_nhds

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#eventually_ge_nhds

English

If b < a, then eventually in nhds(a) we have x ≥ b.

Русский

Если b < a, то в окрестности a существуют x ≥ b.

LaTeX

$$∀ᶠ x ∈ nhds(a), b ≤ x$$

Lean4

theorem eventually_ge_nhds (hab : b < a) : ∀ᶠ x in 𝓝 a, b ≤ x :=
  Ici_mem_nhds hab

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

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

Разделы

Аффилиация

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