mem_nhdsGT — Mathlib

English

If S is order-connected and contains x < y, then S is a punctured right neighbourhood of x.

Русский

Если S упорядочена по связности и содержит x < y, то S является неполной окрестностью справа от x.

LaTeX

$$$$ S\ text{ is OrdConnected},\ hx\in S,\ hy\in S,\ x[> ]x. $$$$

Lean4

/-- If `S` is order-connected and contains two points `x < y`,
then `S` is a punctured right neighbourhood of `x`. -/
theorem mem_nhdsGT (hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[>] x :=
  nhdsWithin_mono _ Ioi_subset_Ici_self <| hS.mem_nhdsGE hx hy hxy

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