mem_nhdsLE

Mathlib.Topology.Order.LeftRightNhds

URI: https://scilib.ai/kg/mathlib#Set.OrdConnected.mem_nhdsLE

← MathLib Explorer

English

If S is order-connected and x < y in S, then S ∈ 𝓝[≤] y.

Русский

Если S упорядочено и x<y в S, тогда S ∈ 𝓝[≤] y.

LaTeX

$$$$ S\text{ is OrdConnected},\ x\in S,\ y\in S,\ x

Lean4

/-- If `S` is order-connected and contains two points `x < y`, then `S` is a left neighbourhood
of `y`. -/
theorem mem_nhdsLE (hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[≤] y :=
  hS.dual.mem_nhdsGE hy hx hxy

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

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

Разделы

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

Аффилиация

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