instNoMinOrderElemIoo — Mathlib

English

In a densely ordered set, the open interval Ioo x y has no minimal element; equivalently, every nonempty subset of Ioo x y has a smaller element.

Русский

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

LaTeX

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

Lean4

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

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