single_antitone — Mathlib

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

Похожие утверждения