good_lt_maxProducts — Mathlib

English

Under suitable assumptions, the two sequences q.val.val and l.val.val are ordered lexicographically by the restricted lt.

Русский

При подходящих предположениях два списка q.val.val и l.val.val упорядочены лексикографически по ограниченному отношению lt.

LaTeX

$$$$\\mathrm{List.Lex}\\big(\\!\\cdot<\\cdot\\!\\big)\\; q.\\mathrm{val}.\\mathrm{val} \\; l.\\mathrm{val}.\\mathrm{val}$$$$

Lean4

theorem good_lt_maxProducts (q : GoodProducts (π C (ord I · < o))) (l : MaxProducts C ho) :
    List.Lex (· < ·) q.val.val l.val.val :=
  by
  have : Inhabited I := ⟨term I ho⟩
  by_cases h : q.val.val = []
  · rw [h, max_eq_o_cons_tail C hsC ho l]
    exact List.Lex.nil
  · rw [← List.cons_head!_tail h, max_eq_o_cons_tail C hsC ho l]
    apply List.Lex.rel
    rw [← Ordinal.typein_lt_typein (· < ·)]
    simp only [term, Ordinal.typein_enum]
    exact Products.prop_of_isGood C _ q.prop q.val.val.head! (List.head!_mem_self h)

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