exists_between — Mathlib

English

In a densely ordered α, for any dense set s and any x<y, there exists z ∈ s with x<z<y.

Русский

В плотно упорядоченном пространстве α для любой плотной множества s и любых x<y существует z ∈ s, такое что x<z<y.

LaTeX

$$$[DenselyOrdered\ α]\;\text{Dense } s \Rightarrow \forall x

Lean4

theorem exists_between [DenselyOrdered α] {s : Set α} (hs : Dense s) {x y : α} (h : x < y) : ∃ z ∈ s, z ∈ Ioo x y :=
  hs.exists_mem_open isOpen_Ioo (nonempty_Ioo.2 h)

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