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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.