English
If X is coindependent, there exists a base B with X ⊆ E \ B.
Русский
Если X коиндепендентно, существует база B такая, что X ⊆ E \ B.
LaTeX
$$coindep_iff_subset_compl_isBase.1 h$$
Lean4
/-- If there is an absolute upper bound on the size of an independent set, then the maximality axiom
isn't needed to define a matroid by independent sets. -/
@[simps E]
protected def ofBdd (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
(indep_subset : ∀ ⦃I J⦄, Indep J → I ⊆ J → Indep I)
(indep_aug : ∀ ⦃I B⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
(subset_ground : ∀ I, Indep I → I ⊆ E) (indep_bdd : ∃ (n : ℕ), ∀ I, Indep I → I.encard ≤ n) : IndepMatroid α
where
E := E
Indep := Indep
indep_empty := indep_empty
indep_subset := indep_subset
indep_aug := indep_aug
indep_maximal X _ := Matroid.existsMaximalSubsetProperty_of_bdd indep_bdd X
subset_ground := subset_ground
