IsOrderCompatible

formal source

 138
 139/-- A standard recognizer R is compatible with a comparative recognizer R_cmp if
 140    indistinguishable configurations are also comparatively equivalent -/
 141def IsOrderCompatible (R : Recognizer C E) (R_cmp : ComparativeRecognizer C E')
 142    (gt_events : Set E') (hp : InducesPreorder R_cmp gt_events) : Prop :=
 143  ∀ c₁ c₂, Indistinguishable R c₁ c₂ → comparativeEquiv R_cmp gt_events c₁ c₂
 144
 145/-- If R is order-compatible, the order descends to the quotient -/
 146theorem order_descends_to_quotient (R : Recognizer C E) (R_cmp : ComparativeRecognizer C E')
 147    (gt_events : Set E') (hp : InducesPreorder R_cmp gt_events)
 148    (hcompat : IsOrderCompatible R R_cmp gt_events hp) :
 149    ∀ c₁ c₂ c₁' c₂', Indistinguishable R c₁ c₁' → Indistinguishable R c₂ c₂' →
 150      notGreaterThan R_cmp gt_events c₁ c₂ → notGreaterThan R_cmp gt_events c₁' c₂' := by
 151  intro c₁ c₂ c₁' c₂' h₁ h₂ hle
 152  have heq₁ := hcompat c₁ c₁' h₁
 153  have heq₂ := hcompat c₂ c₂' h₂
 154  -- c₁' ≤ c₁ ≤ c₂ ≤ c₂'
 155  exact hp.trans c₁' c₂ c₂' (hp.trans c₁' c₁ c₂ heq₁.2 hle) heq₂.1
 156
 157/-! ## Separation by Comparisons -/
 158
 159/-- Two configurations are separated by a comparative recognizer if they are
 160    not comparatively equivalent -/
 161def SeparatedBy (R_cmp : ComparativeRecognizer C E) (gt_events : Set E) (c₁ c₂ : C) : Prop :=
 162  ¬comparativeEquiv R_cmp gt_events c₁ c₂
 163
 164/-- A family of comparative recognizers separates points if any two distinct
 165    configurations are separated by at least one recognizer -/
 166def SeparatesPoints {ι : Type*} (R_family : ι → ComparativeRecognizer C E)
 167    (gt_events : ι → Set E) : Prop :=
 168  ∀ c₁ c₂, c₁ ≠ c₂ → ∃ i, SeparatedBy (R_family i) (gt_events i) c₁ c₂
 169
 170/-! ## Metric-Like Structure -/
 171