order_separated — Mathlib

English

In a linearly ordered set with order topology, for any a1 < a2 there exist open sets U,V with a1 ∈ U, a2 ∈ V and such that every element of U is less than every element of V.

Русский

В линейно упорядоченном множестве с порядка топологией существуют открытые окрестности U и V для двух точек a1 < a2 такие, что каждый элемент U меньше любого элемента V.

LaTeX

$$$\\forall a_1,a_2\\in α\\ (a_1

Lean4

theorem order_separated [OrderTopology α] {a₁ a₂ : α} (h : a₁ < a₂) :
    ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂ :=
  let ⟨x, hx, y, hy, h⟩ := h.exists_disjoint_Iio_Ioi
  ⟨Iio x, Ioi y, isOpen_gt' _, isOpen_lt' _, hx, hy, h⟩
    -- see Note [lower instance priority]

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