ofBddAugment_indep — Mathlib

English

Let E and Indep be as above. The independence predicate of the constructed matroid equals the given Indep predicate.

Русский

Пусть E и Indep заданы подобным образом. Независимость, определяемая построенным матроидом, совпадает с данным предикатом Indep.

LaTeX

$$$\\big(\\mathrm{IndepMatroid.ofBddAugment}\\, E\\, Indep\\, indep\\_empty\\, indep\\_subset\\, indep\\_aug\\, indep\\_bdd\\, subset\\_ground\\big).Indep = Indep$$$

Lean4

@[simp]
theorem ofBddAugment_indep (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).Indep = Indep :=
  rfl

Похожие утверждения