Theorems · Definition · logic and foundations

Order.enum

{α : Type u_1} →
  [inst : LinearOrder α] → [inst_1 : WellFoundedLT α] → [IsRegularCardinalOrder α] → (s : Set α) → IsCofinal s → α ≃o ↑s

Enumerate the elements of a cofinal subset of α by α itself. This is a generalization of Nat.nth.

Defined in

Mathlib.SetTheory.Cardinal.Cofinality.Enum

Cited by

11 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderWellFoundedLTIsRegularCardinalOrder