mem_nhdsLT — Mathlib

English

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

Русский

Если S упорядочено и x < y в S, то S является непокрывающей окрестностью слева от y: S ∈ 𝓝[<] y.

LaTeX

$$$$ S\text{ is OrdConnected},\ hx\in S,\ hy\in S,\ x

Lean4

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

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