isAlternating_symmDiff_left — Mathlib

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

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