ofBaseOfFinite_finite — Mathlib

English

If there is a finite base and a base-exchange property, then the resulting matroid is finite.

Русский

Если есть конечная база и свойство обмена базы, то получившийся матроид конечен.

LaTeX

$$$\\mathrm{Matroid\\,ofBaseOfFinite\\_finite}$$$

Lean4

instance ofBaseOfFinite_finite {E : Set α} (hE : E.Finite) IsBase exists_isBase isBase_exchange subset_ground :
    (Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground).Finite :=
  ⟨hE⟩

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