English
There exists a decidable relation for adjacency in the reduced simple graph along a partition, i.e., the reduced adjacency is decidable.
Русский
Существует разрешимая отношение соседства в уменьшенном графе относительно разбиения.
LaTeX
$$DecidableRel (G.regularityReduced P G ε δ).Adj$$
Lean4
/-- The reduction of the graph `G` along partition `P` has edges between `ε`-uniform pairs of parts
that have edge density at least `δ`. -/
@[simps]
def regularityReduced (ε δ : 𝕜) : SimpleGraph α
where
Adj a b := G.Adj a b ∧ ∃ U ∈ P.parts, ∃ V ∈ P.parts, a ∈ U ∧ b ∈ V ∧ U ≠ V ∧ G.IsUniform ε U V ∧ δ ≤ G.edgeDensity U V
symm a
b := by
rintro ⟨ab, U, UP, V, VP, xU, yV, UV, GUV, εUV⟩
refine ⟨G.symm ab, V, VP, U, UP, yV, xU, UV.symm, GUV.symm, ?_⟩
rwa [edgeDensity_comm]
loopless a h := G.loopless a h.1
