pith. machine review for the scientific record. sign in
theorem proved term proof

metric_from_comparisons

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 193theorem metric_from_comparisons {ι : Type*} [Nonempty ι]
 194    (R_family : ι → ComparativeRecognizer C E)
 195    (gt_events : ι → Set E)
 196    (d : C → C → ℝ)
 197    (hsep : SeparatesPoints R_family gt_events)
 198    (hcompat : ∀ i, MetricCompatible (R_family i) (gt_events i) d) :
 199    -- If c₁ ≠ c₂, then d(c₁, c₂) > 0
 200    ∀ c₁ c₂, c₁ ≠ c₂ → 0 < d c₁ c₂ := by

proof body

Term-mode proof.

 201  intro c₁ c₂ hne
 202  obtain ⟨i, hsep_i⟩ := hsep c₁ c₂ hne
 203  exact (hcompat i).dist_pos_of_separated hsep_i
 204
 205/-! ## The Recognition Distance -/
 206
 207/-- A recognition distance is a pseudometric derived from a family of
 208    comparative recognizers. -/

depends on (17)

Lean names referenced from this declaration's body.