wellFoundedLT — Mathlib

English

The order relation < on ordinals induces a well-founded structure, giving a canonical WellFoundedLT instance on Ordinal.

Русский

Порядок < на ординалах порождает хорошо основанную структуру, задавая канонический экземпляр WellFoundedLT на Ordinal.

LaTeX

$$$\\text{There is a WellFoundedLT structure on } \\mathrm{Ordinal} \\text{ given by } <.$$$

Lean4

instance wellFoundedLT : WellFoundedLT Ordinal :=
  ⟨lt_wf⟩

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