English
If M is a perfect matching and G' is alternating with respect to M.spanningCoe, and G' contains cycles, then the top subgraph of the symmetric difference (M.spanningCoe ∆ G'.spanningCoe) is a perfect matching.
Русский
Если M является совершенным совпадением, и G' чередуется относительно M.spanningCoe, и G' содержит циклы, то верхняя подграфа симметрической разности (M.spanningCoe ∆ G'.spanningCoe) образует совершенное совпадение.
LaTeX
$$$ \text{If } hM : M.IsPerfectMatching,\; hG' : G'.IsAlternating M.spanningCoe,\; hG'cyc : G'.IsCycles, \\ (\top : Subgraph (M.spanningCoe \Delta G')).IsPerfectMatching $$$
Lean4
theorem symmDiff_of_isAlternating (hM : M.IsPerfectMatching) (hG' : G'.IsAlternating M.spanningCoe)
(hG'cyc : G'.IsCycles) : (⊤ : Subgraph (M.spanningCoe ∆ G')).IsPerfectMatching :=
by
rw [Subgraph.isPerfectMatching_iff]
intro v
simp only [symmDiff_def]
obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
by_cases h : G'.Adj v w
· obtain ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj h
have hmadj : M.Adj v w ↔ ¬M.Adj v w' := by simpa using hG' hw'.1 h hw'.2
use w'
simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj, hmadj.mp hw.1, hw'.2,
not_true_eq_false, and_self, not_false_eq_true, or_true, true_and]
rintro y (hl | hr)
· aesop
· obtain ⟨w'', hw''⟩ := hG'cyc.other_adj_of_adj hr.1
by_contra! hc
simp_all [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hc hr.1 hw'.2]
· use w
simp only [Subgraph.top_adj, SimpleGraph.sup_adj, sdiff_adj, Subgraph.spanningCoe_adj, hw.1, h, not_false_eq_true,
and_self, not_true_eq_false, or_false, true_and]
rintro y (hl | hr)
· exact hw.2 _ hl.1
· have ⟨w', hw'⟩ := hG'cyc.other_adj_of_adj hr.1
simp_all [show M.Adj v y ↔ ¬M.Adj v w' from by simpa using hG' hw'.1 hr.1 hw'.2]
