theorem proved term proof

`config_exists`

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

formal statement (Lean)

  62theorem config_exists (C : Type*) [cs : ConfigSpace C] : ∃ c : C, c = ConfigSpace.witness C :=

Term-mode proof.

  63  ⟨ConfigSpace.witness C, rfl⟩
  64
  65/-- An event space has at least two distinct elements -/

Lean names referenced from this declaration's body.