English
The IsBase predicate is preserved under the construction Matroid.ofExistsFiniteIsBase.
Русский
Предикат IsBase сохраняется при построении Matroid.ofExistsFiniteIsBase.
LaTeX
$$$(Matroid.ofExistsFiniteIsBase\\ E\\ IsBase\\ exists_finite_base\\ isBase_exchange\\ subset_ground).IsBase = IsBase$$$
Lean4
/-- A collection of bases with the exchange property and at least one finite member is a matroid -/
@[simps! E]
protected def ofExistsFiniteIsBase (E : Set α) (IsBase : Set α → Prop) (exists_finite_base : ∃ B, IsBase B ∧ B.Finite)
(isBase_exchange : ExchangeProperty IsBase) (subset_ground : ∀ B, IsBase B → B ⊆ E) : Matroid α :=
Matroid.ofBase (E := E) (IsBase := IsBase) (exists_isBase := by obtain ⟨B, h⟩ := exists_finite_base; exact ⟨B, h.1⟩)
(isBase_exchange := isBase_exchange) (maximality :=
by
obtain ⟨B, hB, hfin⟩ := exists_finite_base
refine fun X _ ↦ Matroid.existsMaximalSubsetProperty_of_bdd ⟨B.ncard, fun Y ⟨B', hB', hYB'⟩ ↦ ?_⟩ X
rw [hfin.cast_ncard_eq, isBase_exchange.encard_isBase_eq hB hB']
exact encard_mono hYB') (subset_ground := subset_ground)
