pith. machine review for the scientific record. sign in
class definition def or abbrev

ConfigSpace

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  33class ConfigSpace (C : Type*) where
  34  /-- The configuration space is nonempty -/
  35  nonempty : Nonempty C
  36
  37/-- Extract a witness configuration from a ConfigSpace -/
  38noncomputable def ConfigSpace.witness (C : Type*) [cs : ConfigSpace C] : C :=

proof body

Definition body.

  39  cs.nonempty.some
  40
  41/-! ## Event Space -/
  42
  43/-- An event space is a type of observable outcomes.
  44    Events are things like "the needle points this direction,"
  45    "the detector clicks," or "the image matches this template." -/

used by (24)

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

depends on (19)

Lean names referenced from this declaration's body.