English
There is a preorder on α ⊕ β defined by taking the two component orders and lifting them; the left and right injections are monotone with respect to this preorder.
Русский
На α ⊕ β задан предпорядок, который строится из порядков на α и β путём подъема; инъекции inl и inr монотоновны относительно этого предпорядка.
LaTeX
$$$\text{Preorder on } \alpha \oplus \beta:\; a \le b := \mathrm{LiftRel}(\le_\alpha, \le_\beta)(a,b),\; a < b := \mathrm{LiftRel}(<, <)(a,b)$$$
Lean4
instance instPreorderSum : Preorder (α ⊕ β) :=
{ instLESum, instLTSum with le_refl := fun _ => LiftRel.refl _ _ _, le_trans := fun _ _ _ => LiftRel.trans _ _,
lt_iff_le_not_ge := fun a b =>
by
refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩
· rintro (⟨hba⟩ | ⟨hba⟩)
· exact hba.not_gt (inl_lt_inl_iff.1 hab)
· exact hba.not_gt (inr_lt_inr_iff.1 hab)
· rintro ⟨⟨hab⟩ | ⟨hab⟩, hba⟩
· exact LiftRel.inl (hab.lt_of_not_ge fun h => hba <| LiftRel.inl h)
· exact LiftRel.inr (hab.lt_of_not_ge fun h => hba <| LiftRel.inr h) }
