English
The supremum (join) of two disjointings of matchings is again a matching.
Русский
Объединение двух несовместимых соответствий образует новое соответствие.
LaTeX
$$$$(M \\sqcup M').IsMatching$$$$
Lean4
theorem sup (hM : M.IsMatching) (hM' : M'.IsMatching) (hd : Disjoint M.support M'.support) : (M ⊔ M').IsMatching :=
by
intro v hv
have aux {N N' : Subgraph G} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts) :
∃! w, (N ⊔ N').Adj v w := by
obtain ⟨w, hw⟩ := hN hmN
use w
refine ⟨sup_adj.mpr (.inl hw.1), ?_⟩
intro y hy
cases hy with
| inl h => exact hw.2 y h
| inr h =>
rw [Set.disjoint_left] at hd
simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v
cases Set.mem_or_mem_of_mem_union hv with
| inl hmM => exact aux hM hd hmM
| inr hmM' =>
rw [sup_comm]
exact aux hM' (Disjoint.symm hd) hmM'
