English
From a finite base existence, one obtains a matroid with ground E and IsBase predicate.
Русский
Из существования конечной базы следует матроид с опорным множеством E и предикатом IsBase.
LaTeX
$$$\\mathrm{Matroid.ofExistsFiniteIsBase}\\; E\\; IsBase\\; exists_finite_base\\; isBase_exchange\\; subset_ground$$$
Lean4
/-- If `E` is finite, then any nonempty collection of its subsets
with the exchange property is the collection of bases of a matroid on `E`. -/
protected def ofIsBaseOfFinite {E : Set α} (hE : E.Finite) (IsBase : Set α → Prop) (exists_isBase : ∃ B, IsBase B)
(isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ B, IsBase B → B ⊆ E) : Matroid α :=
Matroid.ofExistsFiniteIsBase (E := E) (IsBase := IsBase) (exists_finite_base :=
let ⟨B, hB⟩ := exists_isBase
⟨B, hB, hE.subset (subset_ground B hB)⟩)
(isBase_exchange := isBase_exchange) (subset_ground := subset_ground)
