English
Given two subgraphs M, M' of G with M and M' both perfect matchings, the symmetric difference of their spanningCoe subgraphs is alternating with respect to M.spanningCoe.
Русский
Пусть M и M' — два подграфа G, каждый из которых является совершенным совпадением. Симметрическая разность их spanningCoe образует чередование относительно 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_left {M' : Subgraph G'} (hM : M.IsPerfectMatching) (hM' : M'.IsPerfectMatching) :
(M.spanningCoe ∆ M'.spanningCoe).IsAlternating M.spanningCoe :=
by
intro v w w' hww' hvw hvw'
obtain ⟨v1, hm1, hv1⟩ := hM.1 (hM.2 v)
obtain ⟨v2, hm2, hv2⟩ := hM'.1 (hM'.2 v)
simp only [symmDiff_def] at *
aesop