ord_term_aux — Mathlib

English

If ho is such that o < type(...) then ord I (term I ho) equals o, as a simp consequence.

Русский

Если допущение обеспечивает o < type(...), то ord I(term I ho) = o (по упрощению).

LaTeX

$$$\\forall o, ho:\\ o<\\mathrm{type}((<)) \\Rightarrow \\mathrm{ord}_I(\\mathrm{term}_I(ho)) = o.$$$

Lean4

@[simp]
theorem ord_term_aux {o : Ordinal} (ho : o < Ordinal.type ((· < ·) : I → I → Prop)) : ord I (term I ho) = o := by
  simp only [ord, term, Ordinal.typein_enum]

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