ofBdd_indep — Mathlib

English

Given a ground E, an independence predicate Indep with a finite bound, there is an IndepMatroid whose matroid component equals the given Indep.

Русский

При заданном E и ограничении независимости Indep существует IndepMatroid, чья связка матроида совпадает с Indep.

LaTeX

$$IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd$$

Lean4

@[simp]
theorem ofBdd_indep (E : Set α) Indep indep_empty indep_subset indep_aug subset_ground h_bdd :
    (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).Indep = Indep :=
  rfl

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