English
There is an order isomorphism between WithBot α and PUnit ⊕ₗ α, sending ⊥ to Unit and ↑a to a.
Русский
Существует изоморфизм порядка между WithBot α и PUnit ⊕ₗ α, отправляющий ⊥ в Unit, а ↑a в a.
LaTeX
$$$\\text{WithBot.orderIsoPUnitSumLex}: WithBot\\,\\alpha \\cong_o (PUnit \\oplus_{\\mathrm{lex}} \\alpha)$$$
Lean4
/-- `WithBot α` is order-isomorphic to `PUnit ⊕ₗ α`, by sending `⊥` to `Unit` and `↑a` to
`a`. -/
def orderIsoPUnitSumLex : WithBot α ≃o PUnit ⊕ₗ α :=
⟨(Equiv.optionEquivSumPUnit α).trans <| (Equiv.sumComm _ _).trans toLex, fun {a b} =>
by
simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk, Equiv.sumComm_apply, swap,
Lex.toLex_le_toLex, le_refl]
cases a <;> cases b
· simp only [elim_inr, lex_inl_inl, bot_le]
· simp only [elim_inr, elim_inl, Lex.sep, bot_le]
· simp only [elim_inl, elim_inr, lex_inr_inl, false_iff]
exact not_coe_le_bot _
· simp only [elim_inl, lex_inr_inr, coe_le_coe]⟩
