single_strictAnti — Mathlib

English

The map a ↦ toLex(singleton a, 1) is strictly anti-monotone: 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 < b \\Rightarrow \\operatorname{toLex}(\\operatorname{single} a\,1) > \\operatorname{toLex}(\\operatorname{single} b\,1)$$$

Lean4

theorem single_strictAnti : StrictAnti (fun (a : α) ↦ toLex (single a 1)) :=
  by
  intro a b h
  simp only [LT.lt, Finsupp.lex_def]
  simp only [ofLex_toLex, Nat.lt_eq]
  use a
  constructor
  · intro d hd
    simp only [Finsupp.single_eq_of_ne hd.ne, Finsupp.single_eq_of_ne (hd.trans h).ne]
  · simp [h.ne']

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