symmDiff_isCycles — Mathlib

English

The symmetric difference of two perfect matchings is a collection of disjoint cycles.

Русский

Симметрическая разность двух совершенных совпадений образует набор непересекающихся циклов.

LaTeX

$$(M.spanningCoe ∆ M'.spanningCoe).IsCycles$$

Lean4

theorem symmDiff_isCycles {M : Subgraph G} {M' : Subgraph G'} (hM : M.IsPerfectMatching) (hM' : M'.IsPerfectMatching) :
    (M.spanningCoe ∆ M'.spanningCoe).IsCycles := by
  intro v
  obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
  obtain ⟨w', hw'⟩ := hM'.1 (hM'.2 v)
  simp only [symmDiff_def, Set.ncard_eq_two, ne_eq, imp_iff_not_or, Set.not_nonempty_iff_eq_empty,
    Set.eq_empty_iff_forall_notMem, SimpleGraph.mem_neighborSet, SimpleGraph.sup_adj, sdiff_adj, spanningCoe_adj,
    not_or, not_and, not_not]
  by_cases hww' : w = w'
  · simp_all [← imp_iff_not_or]
  · right
    use w, w'
    aesop

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