English
Let X be a linear order with LocallyFiniteOrder. For any s ⊆ WithBot X, the induced order on s is densely ordered iff s is subsingleton.
Русский
Пусть X — линейно упорядоченное множество с LocallyFiniteOrder. Для любого подмножества s⊆ WithBot X соответствующий порядок плотно упорядочен тогда и только тогда, когда s является одиночным.
LaTeX
$$$\mathrm{DenselyOrdered}(s) \iff \mathrm{Subsingleton}(s).$$$
Lean4
theorem denselyOrdered_set_iff_subsingleton {s : Set (WithBot X)} : DenselyOrdered s ↔ s.Subsingleton :=
by
refine ⟨fun H ↦ ?_, fun h ↦ h.denselyOrdered⟩
rw [← Set.subsingleton_coe, ← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]
suffices DenselyOrdered (WithBot.some ⁻¹' s) by
rintro ⟨x, y, H⟩
rw [_root_.denselyOrdered_set_iff_subsingleton] at this
obtain ⟨z, hz, hz'⟩ := exists_between H
have hz0 : (⊥ : WithBot X) < z := by simp [(Subtype.coe_lt_coe.mpr hz).trans_le']
replace hz' : WithBot.unbot z.val hz0.ne' < WithBot.unbot y (hz0.trans hz').ne' := by
rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
refine absurd (this ?_ ?_) hz'.ne <;> simp
constructor
simp only [Subtype.exists, Set.mem_preimage, Subtype.forall, Subtype.mk_lt_mk, exists_and_right, exists_prop]
intro x hx y hy hxy
have : (⟨_, hx⟩ : s) < ⟨_, hy⟩ := by simp [hxy]
obtain ⟨z, hz, hz'⟩ := exists_between this
simp only [← Subtype.coe_lt_coe] at hz hz'
refine ⟨WithBot.unbot z (hz.trans_le' (by simp)).ne', ⟨?_, ?_⟩, ?_⟩
· simp
· rw [← WithBot.coe_lt_coe]
simp [hz.trans_le]
· rw [← WithBot.coe_lt_coe]
simp [hz'.trans_le']
