rec — Mathlib

English

For a finite well-ordered α with a given order, the type equals the finite cardinal of α.

Русский

Для конечного упорядоченного множества α тип равен конечной мощности α.

LaTeX

$$$\forall \alpha\, (r)\;[IsWellOrder(\alpha, r)]\;[Fintype(\alpha)]\;: \operatorname{type}(r) = \operatorname{card}(\alpha)$$$

Lean4

/-- Inducts on the base `b` expansion of an ordinal. -/
@[elab_as_elim]
protected def rec (b : Ordinal) {C : Ordinal → Sort*} (H0 : C 0) (H : ∀ o, o ≠ 0 → C (o % b ^ log b o) → C o)
    (o : Ordinal) : C o :=
  if h : o = 0 then h ▸ H0 else H o h (CNF.rec b H0 H (o % b ^ log b o))
termination_by o
decreasing_by exact mod_opow_log_lt_self b h

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