SimpleGraph.IsUniform.symm

theorem SimpleGraph.IsUniform.symm : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : LinearOrderedField 𝕜] {G : SimpleGraph α} [inst_1 : DecidableRel G.Adj] {ε : 𝕜}, Symmetric (G.IsUniform ε)

The theorem `SimpleGraph.IsUniform.symm` asserts that for any type `α`, any linearly ordered field `𝕜`, any simple graph `G` of type `α`, any decidable relationship `G.Adj` on the graph, and any element `ε` of the field `𝕜`, the `SimpleGraph.IsUniform` relation of graph `G` with respect to `ε` is symmetric. In other words, if for any two vertices in the graph `G`, the `IsUniform` relation holds with respect to `ε`, then the same relation holds with the vertices switched, meaning that the relation doesn't depend on the order of the vertices.

More concisely: For any simple graph `G` with a decidable relation `Adj` over a linearly ordered field `𝕜` and any element `ε` in `𝕜`, if `G` is uniform with respect to `ε`, then it is symmetric with respect to `ε`.