Franklin and McNicholl define a metric on a graph by: d_G(v₀,v₁) = 0 if v₀ = v₁ 1 if (v₀,v₁) ∈ E; 2 otherwise
They say this is "clearly" a metric. We prove this formally and generalize it, by replacing 1 and 2 by real numbers 0 < a ≤ 2b, b ≤ 2a (the fact that 0 < b follows but does not need to be mentioned).
noncomputable instance
franklinMcNichollMetric
{U : Type}
(G : SimpleGraph U)
(a : ℝ)
(b : ℝ)
(h₀ : 0 < a)
(h₁ : a ≤ b + b)
(h₂ : b ≤ a + a)
:
Equations
- franklinMcNichollMetric G a b h₀ h₁ h₂ = MetricSpace.mk ⋯