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

InducesPreorder

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)

  76structure InducesPreorder (R : ComparativeRecognizer C E) (gt_events : Set E) : Prop where
  77  /-- The equal event is not a "greater than" event -/
  78  eq_not_gt : R.eq_event ∉ gt_events
  79  /-- Transitivity: c₁ ≤ c₂ and c₂ ≤ c₃ implies c₁ ≤ c₃ -/
  80  trans : ∀ c₁ c₂ c₃, notGreaterThan R gt_events c₁ c₂ →
  81                       notGreaterThan R gt_events c₂ c₃ →
  82                       notGreaterThan R gt_events c₁ c₃
  83
  84/-- When a comparative recognizer induces a preorder, we get reflexivity for free -/

used by (8)

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

depends on (10)

Lean names referenced from this declaration's body.