rank_eq — Mathlib

English

For a well-founded relation r on α, rank_r(a) equals the supremum of succ(rank_r(b)) over all b with r b a.

Русский

Для хорошо основанного отношения r на α верна формула: rank_r(a) = sup {succ(rank_r(b)) : r(b,a)}.

LaTeX

$$$\operatorname{rank}_r(a) = \sup_{b:\, r b a} \operatorname{succ}(\operatorname{rank}_r(b))$$$

Lean4

theorem rank_eq (a : α) : rank r a = ⨆ b : { b // r b a }, Order.succ (rank r b) :=
  (hwf.apply r a).rank_eq

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