ofExistsFiniteIsBase_isBase — Mathlib

English

The Matroid built from a finite base has finite rank.

Русский

Матроид, построенный из конечной базы, имеет конечный ранг.

LaTeX

$$$\\mathrm{Matroid.ofExistsFiniteIsBase}\\;E\\;IsBase\\;\\dots .RankFinite$$$

Lean4

@[simp]
theorem ofExistsFiniteIsBase_isBase (E : Set α) IsBase exists_finite_base isBase_exchange subset_ground :
    (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).IsBase = IsBase :=
  rfl

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