def definition def or abbrev

`enum`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 282noncomputable def enum : ℕ → E.Event :=

Definition body.

 283  Classical.choose (Countable.exists_surjective_nat (E.countable))
 284

From the project-wide theorem graph. These declarations reference this one in their body.

Candidate in IndisputableMonolith.Foundation.Atomicity decl_use
chooseCandidate in IndisputableMonolith.Foundation.Atomicity decl_use
chooseCandidate_some_spec in IndisputableMonolith.Foundation.Atomicity decl_use
enum_surjective in IndisputableMonolith.Foundation.Atomicity decl_use
exists_candidate_index in IndisputableMonolith.Foundation.Atomicity decl_use
minIndex_min in IndisputableMonolith.Foundation.Atomicity decl_use
minIndex_spec in IndisputableMonolith.Foundation.Atomicity decl_use

Lean names referenced from this declaration's body.