SeparatesPoints

formal source

 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
 172/-- A comparative recognizer defines a "distance-like" function when it can
 173    distinguish "closer" from "farther" configurations. -/
 174structure MetricCompatible (R_cmp : ComparativeRecognizer C E) (gt_events : Set E)
 175    (d : C → C → ℝ) : Prop where
 176  /-- d(c,c) = 0 -/
 177  dist_self : ∀ c, d c c = 0
 178  /-- d(c₁,c₂) ≥ 0 -/
 179  dist_nonneg : ∀ c₁ c₂, 0 ≤ d c₁ c₂
 180  /-- d(c₁,c₂) = d(c₂,c₁) -/
 181  dist_symm : ∀ c₁ c₂, d c₁ c₂ = d c₂ c₁
 182  /-- If the recognizer *separates* `c₁,c₂`, then their distance is strictly positive. -/
 183  dist_pos_of_separated : ∀ {c₁ c₂ : C}, SeparatedBy R_cmp gt_events c₁ c₂ → 0 < d c₁ c₂
 184  /-- If c₁ ≤ c₂ (by comparison), then d(c₁, c₃) ≤ d(c₂, c₃) for all c₃ -/
 185  order_respects_dist : ∀ c₁ c₂ c₃, notGreaterThan R_cmp gt_events c₁ c₂ →
 186    d c₁ c₃ ≤ d c₂ c₃
 187
 188/-- **Key Theorem**: Many comparative recognizers can approximate a metric.
 189
 190    The idea: if we have enough comparative recognizers that collectively
 191    separate all points and respect a common distance function, then
 192    that distance function is "visible" through the comparisons. -/
 193theorem metric_from_comparisons {ι : Type*} [Nonempty ι]
 194    (R_family : ι → ComparativeRecognizer C E)
 195    (gt_events : ι → Set E)
 196    (d : C → C → ℝ)