English
If α is a preorder with a bottom element, then the injection with bottom through WithBot defines a Galois insertion between WithBot.unbotD ⊥ and some: α → WithBot α.
Русский
Пусть α — частично упорядоченное множество с нижней границей. Тогда вложение WithBot.unbotD ⊥ и some: α → WithBot α образуют Galois вставку.
LaTeX
$$$\mathrm{WithBot.unbotD} \bottom \dashv\vdash \mathrm{WithBot}.\mathrm{some}$$$
Lean4
/-- If `α` is a partial order with bottom element (e.g., `ℕ`, `ℝ≥0`), then `WithBot.unbot' ⊥` and
coercion form a Galois insertion. -/
def giUnbotDBot [Preorder α] [OrderBot α] : GaloisInsertion (WithBot.unbotD ⊥) (some : α → WithBot α)
where
gc _ _ := WithBot.unbotD_le_iff (fun _ ↦ bot_le)
le_l_u _ := le_rfl
choice o _ := o.unbotD ⊥
choice_eq _ _ := rfl
