finite_setOf_matroid' — Mathlib

English

For finite E, there are finitely many matroids M with ground set exactly E.

Русский

Для конечного E существует конечное множество матроидов M с точным ground E.

LaTeX

$$$ E \\text{ finite} \\Rightarrow \\{M : Matroid \\ α \\mid M.E = E\\}.Finite $$$

Lean4

/-- For finite `E`, finitely many matroids have ground set `E`. -/
theorem finite_setOf_matroid' {E : Set α} (hE : E.Finite) : {M : Matroid α | M.E = E}.Finite :=
  (finite_setOf_matroid hE).subset (fun M ↦ by rintro rfl; exact rfl.subset)

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