ofBddAugment_rankFinite — Mathlib

English

The matroid produced by the bounded-augmentation construction has finite rank.

Русский

Матроид, полученный конструктором bounded augmentation, имеет конечный ранг.

LaTeX

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

Lean4

instance ofBddAugment_rankFinite (E : Set α) Indep indep_empty indep_subset indep_aug indep_bdd subset_ground :
    RankFinite (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).matroid :=
  by
  rw [IndepMatroid.ofBddAugment]
  infer_instance

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