toLex_monotone — Mathlib

English

Let a,b be elements of Lex(Π_i α_i) and i an index. If for all j < i we have the j-th coordinates equal, and a_i < b_i, then a < b in the lexicographic order.

Русский

Пусть a,b — элементы Lex(Π_i α_i) и i — индекс. Если для всех j < i координаты на позиции j равны, а на позиции i a_i < b_i, то a < b в лексикографическом порядке.

LaTeX

$$$$ \\forall a,b,i,\\ (\\forall j

Lean4

theorem toLex_monotone : Monotone (@toLex (Π₀ i, α i)) :=
  by
  intro a b h
  refine le_of_lt_or_eq (or_iff_not_imp_right.2 fun hne ↦ ?_)
  classical
    exact
    ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne), fun j hj ↦ notMem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_gt hj,
      (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩

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