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

inducedPartialOrder

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)

 110def inducedPartialOrder (R : ComparativeRecognizer C E) (gt_events : Set E)
 111    (h : InducesPartialOrder R gt_events) : PartialOrder C where
 112  le := notGreaterThan R gt_events

proof body

Definition body.

 113  le_refl := preorder_refl R gt_events h.toInducesPreorder
 114  le_trans := fun _ _ _ => h.trans _ _ _
 115  le_antisymm := fun _ _ => h.antisymm _ _
 116
 117/-! ## Comparative Equivalence -/
 118
 119/-- Comparative equivalence is an equivalence relation -/

depends on (13)

Lean names referenced from this declaration's body.