English
For finite E, there are only finitely many matroids on α whose ground set is contained in E.
Русский
Для конечного множества E существует лишь конечное число матроидов на α с тем, что их множество оснований E содержит в E.
LaTeX
$$$ E \\text{ finite} \\Rightarrow \\{M : Matroid \\ α \\mid M.E \\subseteq E\\}.Finite $$$
Lean4
/-- For finite `E`, finitely many matroids have ground set contained in `E`. -/
theorem finite_setOf_matroid {E : Set α} (hE : E.Finite) : {M : Matroid α | M.E ⊆ E}.Finite :=
by
set f : Matroid α → Set α × (Set (Set α)) := fun M ↦ ⟨M.E, {B | M.IsBase B}⟩
have hf : f.Injective := by
refine fun M M' hMM' ↦ ?_
rw [Prod.mk.injEq, and_comm, Set.ext_iff, and_comm] at hMM'
exact ext_isBase hMM'.1 (fun B _ ↦ hMM'.2 B)
rw [← Set.finite_image_iff hf.injOn]
refine (hE.finite_subsets.prod hE.finite_subsets.finite_subsets).subset ?_
rintro _ ⟨M, hE : M.E ⊆ E, rfl⟩
simp only [Set.mem_prod, Set.mem_setOf_eq]
exact ⟨hE, fun B hB ↦ hB.subset_ground.trans hE⟩
