exists_finset_isBasis' — Mathlib

English

An IsRkFinite X matroid has a finite finset basis 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 finset basis' -/
theorem exists_finset_isBasis' (h : M.IsRkFinite X) : ∃ (I : Finset α), M.IsBasis' I X :=
  let ⟨I, hI, hIfin⟩ := h.exists_finite_isBasis'
  ⟨hIfin.toFinset, by simpa⟩

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