structure definition def or abbrev

`Candidate`

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

formal statement (Lean)

 315structure Candidate (picked : Finset E.Event) where
 316  idx : ℕ
 317  event : E.Event
 318  event_def : enum (E:=E) idx = event

Definition body.

 319  not_mem : event ∉ picked
 320  eligible_event : eligible (ev:=ev) picked event
 321

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

ConvergenceHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
ECDLPInstance in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
chooseCandidate in IndisputableMonolith.Foundation.Atomicity decl_use
chooseCandidate_some_spec in IndisputableMonolith.Foundation.Atomicity decl_use
correction_D_half in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use
correction_D_quad1 in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use
correction_E_eighth in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use
correction_F_quarter in IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity decl_use

Lean names referenced from this declaration's body.