finite — Mathlib

English

As above: the finite size of the matching set.

Русский

Аналогично: множество матчингoв конечное.

LaTeX

$$$\\\\text{Finite}(\\\\mathrm{hallMatchingsOn}(t,\\\\iota')).$$$

Lean4

instance finite {ι : Type u} {α : Type v} (t : ι → Finset α) (ι' : Finset ι) : Finite (hallMatchingsOn t ι') := by
  classical
  rw [hallMatchingsOn]
  let g : hallMatchingsOn t ι' → ι' → ι'.biUnion t := by
    rintro f i
    refine ⟨f.val i, ?_⟩
    rw [mem_biUnion]
    exact ⟨i, i.property, f.property.2 i⟩
  apply Finite.of_injective g
  intro f f' h
  ext a
  rw [funext_iff] at h
  simpa [g] using h a

Похожие утверждения