def
definition
inducedPartialOrder
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Comparative on GitHub at line 110.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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₃) :
134 comparativeEquiv R gt_events c₁ c₃ :=
135 ⟨hp.trans c₁ c₂ c₃ h₁.1 h₂.1, hp.trans c₃ c₂ c₁ h₂.2 h₁.2⟩
136
137/-! ## Order-Respecting Recognizers -/
138
139/-- A standard recognizer R is compatible with a comparative recognizer R_cmp if
140 indistinguishable configurations are also comparatively equivalent -/