class definition def or abbrev

`DecEventSpace`

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

formal statement (Lean)

  52class DecEventSpace (E : Type*) extends EventSpace E where
  53  /-- Decidable equality on events -/
  54  decEq : DecidableEq E
  55
  56attribute [instance] DecEventSpace.decEq
  57
  58/-! ## Basic Properties -/
  59
  60/-- **THEOREM**: A configuration space has at least one element.
  61    Replaces the vacuous `∃ c : C, True` with a constructive witness. -/

depends on (10)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
EventSpace in IndisputableMonolith.RecogGeom.Core decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use