English
There is a Galois insertion between toRegular and coe, i.e., toRegular is left adjoint to the inclusion.
Русский
Существуeт Галуа-вставка между toRegular и включением, то есть toRegular является левым смежным к включению.
LaTeX
$$$\mathrm{gi} : \mathrm{GaloisInsertion}(toRegular, (\uparrow))$$$
Lean4
/-- The Galois insertion between `Regular.toRegular` and `coe`. -/
def gi : GaloisInsertion toRegular ((↑) : Regular α → α)
where
choice a ha := ⟨a, ha.antisymm le_compl_compl⟩
gc _ b := coe_le_coe.symm.trans <| ⟨le_compl_compl.trans, fun h => (compl_anti <| compl_anti h).trans_eq b.2⟩
le_l_u _ := le_compl_compl
choice_eq _ ha := coe_injective <| le_compl_compl.antisymm ha
