nhdsWithin_Ioi_neBot'

Mathlib.Topology.Order.DenselyOrdered

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

← MathLib Explorer

English

If there exists b > a, then the right-sided neighborhood at a, 𝓝[> ] a, is nontrivial (NeBot).

Русский

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

LaTeX

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

Lean4

theorem nhdsWithin_Ioi_neBot' {a b : α} (H₁ : (Ioi a).Nonempty) (H₂ : a ≤ b) : NeBot (𝓝[Ioi a] b) :=
  mem_closure_iff_nhdsWithin_neBot.1 <| by rwa [closure_Ioi' H₁]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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