instNoMinOrderElemIoi — Mathlib

English

In a densely ordered set, the open interval Ioo x y has no maximal element; equivalently, for every a ∈ Ioo x y there exists b ∈ Ioo x y with a < b.

Русский

В плотно упорядоченном множестве открытый интервал (x,y) не имеет максимального элемента; для любого a ∈ (x,y) существует b ∈ (x,y) с a < b.

LaTeX

$$NoMaxOrder (Set.Ioo x y)$$

Lean4

instance : NoMinOrder (Set.Ioi x) :=
  ⟨fun ⟨a, ha⟩ => by
    rcases exists_between ha with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, hb₁⟩, hb₂⟩⟩

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