isBase_restrict_iff' — Mathlib

English

Let M be a matroid, I a subset, and X a subset of the ground set. Then (M|X) isBase on I if and only if I is a basis of M with respect to X, i.e., M.IsBasis' I X.

Русский

Пусть M — матроид, I ⊆ α и X ⊆ α. Тогда I является базисом ограниченного матроидa M|X относительно I тогда и только тогда, когда I является базисом M относительно X (M.IsBasis' I X).

LaTeX

$$$ (M|X).IsBase I \\iff M.IsBasis' I X $$$

Lean4

theorem isBase_restrict_iff' : (M ↾ X).IsBase I ↔ M.IsBasis' I X := by
  simp_rw [isBase_iff_maximal_indep, IsBasis', maximal_iff, restrict_indep_iff]

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