English
The supremum over an index family of pairwise disjoint matchings is again a matching.
Русский
Супремум по индексированному семейству попарно несводимых соответствий остаётся соответствием.
LaTeX
$$$$(\\bigsqcup_i f_i).IsMatching$$$$
Lean4
theorem iSup {ι : Sort _} {f : ι → Subgraph G} (hM : (i : ι) → (f i).IsMatching)
(hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support) : (⨆ i, f i).IsMatching :=
by
intro v hv
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (verts_iSup ▸ hv)
obtain ⟨w, hw⟩ := hM i hi
use w
refine ⟨iSup_adj.mpr ⟨i, hw.1⟩, ?_⟩
intro y hy
obtain ⟨i', hi'⟩ := iSup_adj.mp hy
by_cases heq : i = i'
· exact hw.2 y (heq.symm ▸ hi')
· have := hd heq
simp only [Set.disjoint_left] at this
simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, hi'⟩] using @this v
