inducedPreorder

formal source

  90  exact h.eq_not_gt
  91
  92/-- The induced preorder relation -/
  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
  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₂ -/
 103structure InducesPartialOrder (R : ComparativeRecognizer C E) (gt_events : Set E)
 104    extends InducesPreorder R gt_events : Prop where
 105  /-- Antisymmetry -/
 106  antisymm : ∀ c₁ c₂, notGreaterThan R gt_events c₁ c₂ →
 107                       notGreaterThan R gt_events c₂ c₁ → c₁ = c₂
 108
 109/-- The induced partial order relation -/
 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
 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 -/
 120theorem comparativeEquiv_refl (R : ComparativeRecognizer C E) (gt_events : Set E)
 121    (h : InducesPreorder R gt_events) (c : C) :
 122    comparativeEquiv R gt_events c c :=
 123  ⟨preorder_refl R gt_events h c, preorder_refl R gt_events h c⟩