isBasis_inter_ground — Mathlib

English

Let M be a matroid with ground set E. If I is a basis of X, then I is a basis of X ∩ E.

Русский

Пусть M — матроид над множеством оснований E. Если I является базисом множества X, тогда I является базисом множества X ∩ E.

LaTeX

$$$ M.IsBasis I X \Rightarrow M.IsBasis I (X \cap M.E) $$$

Lean4

theorem isBasis_inter_ground (hI : M.IsBasis I X) : M.IsBasis I (X ∩ M.E) :=
  by
  convert hI
  rw [inter_eq_self_of_subset_left hI.subset_ground]

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