English
WithBot α is densely ordered if and only if α is densely ordered, under [LT α] and [NoMinOrder α].
Русский
WithBot α плотно упорядочен тогда и только тогда, когда α плотно упорядочен, при данных [LT α] и [NoMinOrder α].
LaTeX
$$$DenselyOrdered(WithBot \alpha) \iff DenselyOrdered(\alpha)$$$
Lean4
theorem denselyOrdered_iff [LT α] [NoMinOrder α] : DenselyOrdered (WithBot α) ↔ DenselyOrdered α :=
by
constructor <;> intro h <;> constructor
· intro a b hab
obtain ⟨c, hc⟩ := exists_between (WithBot.coe_lt_coe.mpr hab)
induction c with
| bot => simp at hc
| coe c => exact ⟨c, by simpa using hc⟩
· simpa [WithBot.exists, WithBot.forall, exists_lt] using DenselyOrdered.dense
