ord_eq — Mathlib

English

There exists a well-order on α whose order type is ord #α.

Русский

Существует порядок на α, чей тип порядка равен ord #α.

LaTeX

$$$\exists r\ (wo:\ IsWellOrder \ α \ r),\ ord(#α) = @type α r wo$$$

Lean4

/-- There exists a well-order on `α` whose order type is exactly `ord #α`. -/
theorem ord_eq (α) : ∃ (r : α → α → Prop) (wo : IsWellOrder α r), ord #α = @type α r wo :=
  let ⟨r, wo⟩ := ciInf_mem fun r : { r // IsWellOrder α r } => @type α r.1 r.2
  ⟨r.1, r.2, wo.symm⟩

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