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₂⟩⟩