Unit-distance graph

unitDistanceGraphdef

The unit-distance graph on a metric space joins two points exactly when they are at distance one. Over the Euclidean plane, its chromatic number is the Hadwiger–Nelson problem.

def unitDistanceGraph (X : Type*) [MetricSpace X] : SimpleGraph X where
  Adj x y := x ≠ y ∧ dist x y = 1
  symm := ⟨fun _ _ h => ⟨h.1.symm, by rw [dist_comm]; exact h.2⟩⟩
  loopless := ⟨fun _ h => h.1 rfl⟩

Used by

Problem GT-001 — the Hadwiger–Nelson problem

From Mathlib

Combinatorics.SimpleGraph.Basic
Topology.MetricSpace.Defs

import Conjectura.Defs.Mathematics.Combinatorics.GraphTheory.UnitDistanceGraph · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits