eventually_lt_nhds

Mathlib.Topology.Order.OrderClosed

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

English

For any a < b, there exists a neighborhood of a consisting of elements less than b; equivalently, ∀ᶠ x in 𝓝 a, x < b.

Русский

Для любых a < b существует окрестность точки a, состоящая из элементов меньше b; эквивалентно ∀ᶠ x ∈ 𝓝 a, x < b.

LaTeX

$$$\forall {a,b} \ (a

Lean4

theorem eventually_lt_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x < b :=
  Iio_mem_nhds hab

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

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

Разделы

Аффилиация

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