isAlternating_symmDiff_right — Mathlib

English

If M and M' are perfect matchings, then the symmetric difference is alternating with respect to M'.spanningCoe.

Русский

Если M и M' — совершенные совпадения, то симметрическая разность чередуется относительно M'.spanningCoe.

LaTeX

$$$ \forall {V} {G G' : SimpleGraph V} {M : G.Subgraph} {M' : G'.Subgraph},\; M.IsPerfectMatching \to M'.IsPerfectMatching \to (M.spanningCoe \Delta M'.spanningCoe).IsAlternating M'.spanningCoe $$$

Lean4

theorem isAlternating_symmDiff_right {M' : Subgraph G'} (hM : M.IsPerfectMatching) (hM' : M'.IsPerfectMatching) :
    (M.spanningCoe ∆ M'.spanningCoe).IsAlternating M'.spanningCoe := by
  simpa [symmDiff_comm] using isAlternating_symmDiff_left hM' hM

Похожие утверждения