lt_wf — Mathlib

English

The less-than relation on Nimbers is well-founded; in particular, Nimbers carry a well-founded ordering with respect to <.

Русский

Порядок по сравнению Nimber по отношению к < является хорошо основанным; для Nimber существует хорошо основанный порядок относительно <.

LaTeX

$$$(<) ext{ on Nimbers is WellFounded}$$$

Lean4

theorem lt_wf : @WellFounded Nimber (· < ·) :=
  Ordinal.lt_wf

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