isBasis'_iff_isBasis_restrict_univ

English

A basis in M with respect to I, X is equivalent to I being a basis in the unrestricted matroid M restricted to univ.

Русский

Базис в M по I, X эквивалентен тому, что I образует базис в неограниченном матроиде M на всём множества.

LaTeX

$$$ M.IsBasis' I X \\iff (M \\restriction \\mathrm{univ}).IsBasis I X $$$

Lean4

theorem isBasis'_iff_isBasis_restrict_univ : M.IsBasis' I X ↔ (M ↾ univ).IsBasis I X := by
  rw [isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground, and_iff_left (subset_univ _)]

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