English
Restriction of a matchings on a larger finite set to a smaller subset yields a valid matching on the smaller set.
Русский
Ограничение матчинга, заданного на большем конечном множестве, к подмножеству даёт допустимый матчинг на меньшем множестве.
LaTeX
$$$\\\\text{If } f \\\\in \\\\mathrm{hallMatchingsOn}(t,\\\\iota''), \\\\iota' \\\\subseteq \\\\iota'', \\\\text{then } f|_{\\\\iota'} \\\\in \\\\mathrm{hallMatchingsOn}(t,\\\\iota').$$$
Lean4
/-- Given a matching on a finset, construct the restriction of that matching to a subset. -/
def restrict {ι : Type u} {α : Type v} (t : ι → Finset α) {ι' ι'' : Finset ι} (h : ι' ⊆ ι'')
(f : hallMatchingsOn t ι'') : hallMatchingsOn t ι' :=
by
refine ⟨fun i => f.val ⟨i, h i.property⟩, ?_⟩
obtain ⟨hinj, hc⟩ := f.property
refine ⟨?_, fun i => hc ⟨i, h i.property⟩⟩
rintro ⟨i, hi⟩ ⟨j, hj⟩ hh
simpa only [Subtype.mk_eq_mk] using hinj hh
