InducesPartialOrder

formal source

 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⟩
 124
 125theorem comparativeEquiv_symm (R : ComparativeRecognizer C E) (gt_events : Set E)
 126    {c₁ c₂ : C} (h : comparativeEquiv R gt_events c₁ c₂) :
 127    comparativeEquiv R gt_events c₂ c₁ :=
 128  ⟨h.2, h.1⟩
 129
 130theorem comparativeEquiv_trans (R : ComparativeRecognizer C E) (gt_events : Set E)
 131    (hp : InducesPreorder R gt_events)
 132    {c₁ c₂ c₃ : C} (h₁ : comparativeEquiv R gt_events c₁ c₂)
 133    (h₂ : comparativeEquiv R gt_events c₂ c₃) :