English
There exists a finite base for which the base property holds in a matroid built from finite bases with exchange property.
Русский
Существует конечная база, для которой выполняется свойство базы в матроиде, построенном из конечных баз с обменной свойством.
LaTeX
$$$\\exists B, IsBase B \\land B.Finite$$$
Lean4
/-- A matroid defined purely in terms of its bases. -/
@[simps E]
protected def ofBase (E : Set α) (IsBase : Set α → Prop) (exists_isBase : ∃ B, IsBase B)
(isBase_exchange : ExchangeProperty IsBase)
(maximality : ∀ X, X ⊆ E → Matroid.ExistsMaximalSubsetProperty (∃ B, IsBase B ∧ · ⊆ B) X)
(subset_ground : ∀ B, IsBase B → B ⊆ E) : Matroid α
where
E := E
IsBase := IsBase
Indep I := (∃ B, IsBase B ∧ I ⊆ B)
indep_iff' _ := Iff.rfl
exists_isBase := exists_isBase
isBase_exchange := isBase_exchange
maximality := maximality
subset_ground := subset_ground
