English
The map toLex from the sum α ⊕ β is monotone with respect to the Lex order, i.e., it preserves the order.
Русский
Отображение toLex из суммы α ⊕ β монотонно относительно лексикографического порядка; оно сохраняет порядок.
LaTeX
$$$\\text{Monotone}(\\,\\text{toLex}\\,)$$$
Lean4
instance preorder : Preorder (α ⊕ₗ β) :=
{ Lex.LE, Lex.LT with le_refl := refl_of (Lex (· ≤ ·) (· ≤ ·)),
le_trans := fun _ _ _ => trans_of (Lex (· ≤ ·) (· ≤ ·)),
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⟩ | ⟨b, a⟩)
· exact hba.not_gt (inl_lt_inl_iff.1 hab)
· exact hba.not_gt (inr_lt_inr_iff.1 hab)
· exact not_inr_lt_inl hab
· rintro ⟨⟨hab⟩ | ⟨hab⟩ | ⟨a, b⟩, hba⟩
· exact Lex.inl (hab.lt_of_not_ge fun h => hba <| Lex.inl h)
· exact Lex.inr (hab.lt_of_not_ge fun h => hba <| Lex.inr h)
· exact Lex.sep _ _ }
