exists_isBasis_inter_ground_isBasis_closure

English

For any M and X, there exists I such that I is a basis of X ∩ E and I is a basis of closure X.

Русский

Для любого M и X существует I, такая что I является базисом X ∩ E и базисом замыкания X.

LaTeX

$$$\exists I\ M.IsBasis I (X \cap M.E) \land M.IsBasis I (M.closure X)$$$

Lean4

theorem exists_isBasis_inter_ground_isBasis_closure (M : Matroid α) (X : Set α) :
    ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X) :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)
  have hI' := hI.isBasis_closure_right; rw [closure_inter_ground] at hI'
  exact ⟨_, hI, hI'⟩

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