subset_finite_isBasis'_of_subset_of_isRkFinite

English

Let I be a subset of X that is independent in M, and suppose X has finite rank. Then there exists a set J such that J is a basis of X, I ⊆ J, and J is finite.

Русский

Пусть I ⊆ X и I независимо в матроидe M, причём X имеет конечный ранг. Тогда существует множество J, такое что J является базисом X, I ⊆ J и J конечно.

LaTeX

$$$M.IsRkFinite X \land I \subseteq X \land M.Indep I \Rightarrow \exists J\, (M.IsBasis' J X \land I \subseteq J \land J.Finite)$$$

Lean4

theorem subset_finite_isBasis'_of_subset_of_isRkFinite (hI : M.Indep I) (hIX : I ⊆ X) (hX : M.IsRkFinite X) :
    ∃ J, M.IsBasis' J X ∧ I ⊆ J ∧ J.Finite :=
  (hI.subset_isBasis'_of_subset hIX).imp fun _ hJ => ⟨hJ.1, hJ.2, hJ.1.finite_of_isRkFinite hX⟩

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