head_lt_ord_of_isGood — Mathlib

English

If l is good for a projection π C (ord I · < o) and l.val is nonempty, then ord I (head of l.val) < o.

Русский

Если l является хорошим относительно проекции π C (ord I · < o) и l.val непуст, то ord I (голова списка) меньше o.

LaTeX

$$$[Inhabited I] \\to\\quad \\forall l : Profinite.NobelingProof.Products I\\, \\forall o : Ordinal, (h : l.isGood (π C (ord I · < o))) (hn : l.val \\neq []) : ord I (l.val.head!) < o.$$

Lean4

theorem head_lt_ord_of_isGood [Inhabited I] {l : Products I} {o : Ordinal} (h : l.isGood (π C (ord I · < o)))
    (hn : l.val ≠ []) : ord I (l.val.head!) < o :=
  prop_of_isGood C (ord I · < o) h l.val.head! (List.head!_mem_self hn)

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