English
Let gi be a Galois coinsertion between α and β. If β is a bounded order (i.e., has both a top and a bottom), then α inherits a bounded order structure by combining the lifted bottom from β via liftOrderBot and the lifted top from β via liftOrderTop.
Русский
Пусть gi — коинсерция Гало между α и β. Если β является ограниченно упорядоченным, то α наследует структуру ограниченного порядка, объединяя поднятый нижний предел через liftOrderBot и поднятый верхний предел через liftOrderTop.
LaTeX
$$$\mathrm{GaloisCoinsertion}\;l\,u \Rightarrow \mathrm{BoundedOrder}(\alpha)\;\text{with bottom and top given by lifts of }β$$$
Lean4
/-- Lift the top, bottom, suprema, and infima along a Galois coinsertion -/
abbrev liftBoundedOrder [Preorder β] [BoundedOrder β] (gi : GaloisCoinsertion l u) : BoundedOrder α :=
{ gi.liftOrderBot, gi.gc.liftOrderTop with }
-- See note [reducible non-instances]
