nhdsGT_neBot_of_exists_gt

Mathlib.Topology.Order.DenselyOrdered

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

English

If there exists b > a, then the right-hand neighborhood 𝓝[> a] b is nontrivial.

Русский

Если существует b > a, то 𝓝[> a] b ненулевая.

LaTeX

$$$\exists b\,(a]} b\bigr)$$$

Lean4

theorem nhdsGT_neBot_of_exists_gt {a : α} (H : ∃ b, a < b) : NeBot (𝓝[>] a) :=
  nhdsWithin_Ioi_neBot' H (le_refl a)

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

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

Разделы

Аффилиация

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