mem_nhdsGE — Mathlib

English

If S is order-connected and x, y ∈ S with x < y, then S is a right neighbourhood of x, i.e., S ∈ 𝓝[≥] x.

Русский

Если S имеет связь по порядку и x < y оба в S, то S содержит окрестность справа от x: S ∈ 𝓝[≥] x.

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 right neighbourhood of `x`. -/
theorem mem_nhdsGE (hS : OrdConnected S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) : S ∈ 𝓝[≥] x :=
  mem_of_superset (Icc_mem_nhdsGE hxy) <| hS.out hx hy

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