type_fintype — Mathlib

English

If α is well-ordered and finite, then the type of the well-ordering equals the cardinality of α.

Русский

Если множество α упорядочено в порядке благоприятном для WellOrdered, и оно конечное, то тип упорядочения равен мощности α.

LaTeX

$$$\forall \alpha\,\text{IsWellOrder}(\alpha, r)\;\Rightarrow\; \operatorname{type}(r) = |\alpha|$$$

Lean4

@[simp]
theorem type_fintype (r : α → α → Prop) [IsWellOrder α r] [Fintype α] : type r = Fintype.card α := by
  rw [← card_eq_nat, card_type, mk_fintype]

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