IsAlternating — Mathlib

Lean4
/-- A graph `G` is alternating with respect to some other graph `G'`, if exactly every other edge in
`G` is in `G'`. Note that the degree of each vertex needs to be at most 2 for this to be
possible. This property is used to create new matchings using `symmDiff`.
The definition of `symmDiff` that makes sense is the one for `SimpleGraph`. The `symmDiff`
for `SimpleGraph.Subgraph` deriving from the lattice structure also affects the vertices included,
which we do not want in this case. This is why this property, just like `IsCycles`, is defined
for `SimpleGraph` rather than `SimpleGraph.Subgraph`.
-/
def IsAlternating (G G' : SimpleGraph V) :=
  ∀ ⦃v w w' : V⦄, w ≠ w' → G.Adj v w → G.Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')
Похожие утверждения