English
Let E be a subset of α and let Indep be an independence predicate on subsets of α satisfying the usual independence axioms, together with the augmentation and ground-subset requirements. Then the matroid obtained by the bounded-augmentation construction has ground exactly E.
Русский
Пусть E ⊆ α и Indep — предикат независимости подмножеств α, удовлетворяющий обычным аксиомам независимости, а также условия дополнения и подмножества к опорному множеству. Тогда матроид, полученный конструктором bounded-augmentation, имеет опорное множество, равное E.
LaTeX
$$$\\big(\\mathrm{IndepMatroid.ofBddAugment}\\, E\\, Indep\\, indep\\_empty\\, indep\\_subset\\, indep\\_aug\\, indep\\_bdd\\, subset\\_ground\\big).E = E$$$
Lean4
@[simp]
theorem ofBddAugment_E (E : Set α) Indep indep_empty indep_subset indep_aug indep_bdd subset_ground :
(IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).E = E :=
rfl
