English
The map a ↦ toLex(single a 1) is antitone: if a ≤ b then toLex(single a 1) ≥ toLex(single b 1).
Русский
Отображение a ↦ toLex(single a 1) антитонично: если a ≤ b, то toLex(single a 1) ≥ toLex(single b 1).
LaTeX
$$$\\forall a,b,\\ a \\le b \\Rightarrow \\operatorname{toLex}(\\operatorname{single} a\\,1) \\ge \\operatorname{toLex}(\\operatorname{single} b\\,1)$$$
Lean4
theorem single_antitone : Antitone (fun (a : α) ↦ toLex (single a 1)) :=
Lex.single_strictAnti.antitone