English
This is the definition of the set of matchings for a family t on a finite index set ι': it consists of injective maps f: ι' → α with f(i) ∈ t(i) for all i ∈ ι'.
Русский
Это определение множества матчинг-объединений (matchings) для семейства t на конечном индексе ι': это множество инъективных отображений f: ι' → α с условием f(i) ∈ t(i) для всех i.
LaTeX
$$$\\\\mathrm{hallMatchingsOn}(t,\\\\iota') = {f:\\\\iota' \\\\to \\\\alpha \\\\mid\\\\ \\\\text{Injective}(f) \\\\wedge\\\\ \\\\forall x:{ x \\\\in \\\\iota'}, f(x) \\\\in t(x)}.$$$
Lean4
/-- The set of matchings for `t` when restricted to a `Finset` of `ι`. -/
def hallMatchingsOn {ι : Type u} {α : Type v} (t : ι → Finset α) (ι' : Finset ι) :=
{f : ι' → α | Function.Injective f ∧ ∀ (x : { x // x ∈ ι' }), f x ∈ t x}
