toLex_monotone — Mathlib

English

The map that sends a function a to its lexicographic representation toLex(a) is monotone with respect to the natural pointwise order on the Pi-type.

Русский

Отображение a ↦ toLex(a) монотонно относительно естественного покомпонентного порядка на Pi-типе.

LaTeX

$$$(a,b)\\in (\\forall i, \\beta i)\\times(\\forall i, \\beta i) : a \\le b \\Rightarrow \\mathrm{toLex}(a) \\le \\mathrm{toLex}(b).$$$

Lean4

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

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