head!_eq_o_of_maxProducts — Mathlib

English

A strengthened variant: a maximal product equals term :: tail under chain conditions.

Русский

Усиленная версия: максимальный продукт равен term :: tail при условиях цепи.

LaTeX

$$$\\text{max\\_eq\\_o\\_cons\\_tail'} C ho l$$$

Lean4

theorem head!_eq_o_of_maxProducts [Inhabited I] (l : ↑(MaxProducts C ho)) : l.val.val.head! = term I ho :=
  by
  rw [eq_comm, ← ord_term ho]
  have hm := l.prop.2
  have :=
    Products.prop_of_isGood_of_contained C _ l.prop.1 hsC l.val.val.head! (List.head!_mem_self (List.ne_nil_of_mem hm))
  simp only [Order.lt_succ_iff] at this
  refine eq_of_le_of_not_lt this (not_lt.mpr ?_)
  have h : ord I (term I ho) ≤ ord I l.val.val.head! :=
    by
    simp only [ord, Ordinal.typein_le_typein, not_lt]
    exact Products.rel_head!_of_mem hm
  rwa [ord_term_aux] at h

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