exists_finite_isBasis' — Mathlib

English

An IsRkFinite X matroid has a finite index basis I that is a basis' for X, i.e., a Finset I with M.IsBasis' I X.

Русский

У матроидa IsRkFinite X существует конечный по размеру базис I, такой что M.IsBasis' I X.

LaTeX

$$$ \\exists (I : Finset \\alpha), M.IsBasis' I X $$$

Lean4

/-- An `IsRkFinite` set has a finite basis' -/
theorem exists_finite_isBasis' (h : M.IsRkFinite X) : ∃ I, M.IsBasis' I X ∧ I.Finite :=
  h.exists_finite_isBase

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