toLex_strictMono — Mathlib

English

The map a ↦ toLex(a) is strictly monotone on the Pi-type: if a < b then toLex(a) < toLex(b).

Русский

Отображение a ↦ toLex(a) строго монотонно по отношению к Pi-типу: если a < b, то toLex(a) < toLex(b).

LaTeX

$$$\\text{If } a < b \\text{ then } \\mathrm{toLex}(a) < \\mathrm{toLex}(b).$$$

Lean4

theorem toLex_strictMono : StrictMono (@toLex (∀ i, β i)) := fun a b h =>
  let ⟨i, hi, hl⟩ := IsWellFounded.wf.has_min (r := (· < ·)) {i | a i ≠ b i} (Function.ne_iff.1 h.ne)
  ⟨i, fun j hj => by
    contrapose! hl
    exact ⟨j, hl, hj⟩, (h.le i).lt_of_ne hi⟩

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