Unit-distance graph

Conjectura.Defs.Mathematics.Combinatorics.GraphTheory.UnitDistanceGraph

/-
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
-/
import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Topology.MetricSpace.Defs

/-! # Unit-distance graph -/

namespace Conjectura.GraphTheory

/-- 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⟩

end Conjectura.GraphTheory