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

inducedPreorder

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)

  93def inducedPreorder (R : ComparativeRecognizer C E) (gt_events : Set E)
  94    (h : InducesPreorder R gt_events) : Preorder C where
  95  le := notGreaterThan R gt_events

proof body

Definition body.

  96  le_refl := preorder_refl R gt_events h
  97  le_trans := fun _ _ _ => h.trans _ _ _
  98
  99/-! ## Recognition Partial Order -/
 100
 101/-- A comparative recognizer induces a partial order when it's also antisymmetric:
 102    c₁ ≤ c₂ and c₂ ≤ c₁ implies c₁ = c₂ -/

depends on (12)

Lean names referenced from this declaration's body.