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

ComparativeRecognizer

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)

  50structure ComparativeRecognizer (C E : Type*) where
  51  /-- The comparison function -/
  52  compare : C × C → E
  53  /-- Reflexivity: comparing c with itself gives a distinguished "equal" result -/
  54  eq_event : E
  55  /-- Self-comparison yields the equal event -/
  56  compare_self : ∀ c, compare (c, c) = eq_event
  57
  58/-! ## Induced Relations -/
  59
  60variable {E : Type*} [DecidableEq E]
  61
  62/-- The "not greater than" relation induced by a comparative recognizer.
  63    c₁ ≤ c₂ iff comparing them doesn't produce a "greater than" result. -/

used by (18)

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

depends on (2)

Lean names referenced from this declaration's body.