English
For M, M' and X: M|X = M'|X iff for all I ⊆ X, M.Indep I ↔ M'.Indep I.
Русский
Для M, M' и X: M|X = M'|X тогда и только тогда, когда для всех I ⊆ X выполняется M.Indep I ↔ M'.Indep I.
LaTeX
$$$ M \\restriction X = M' \\restriction X \\iff \\forall I \\subseteq X, M.Indep I \\iff M'.Indep I $$$
Lean4
theorem restrict_eq_restrict_iff (M M' : Matroid α) (X : Set α) :
M ↾ X = M' ↾ X ↔ ∀ I, I ⊆ X → (M.Indep I ↔ M'.Indep I) :=
by
refine ⟨fun h I hIX ↦ ?_, fun h ↦ ext_indep rfl fun I (hI : I ⊆ X) ↦ ?_⟩
·
rw [← and_iff_left (a := (M.Indep I)) hIX, ← and_iff_left (a := (M'.Indep I)) hIX, ← restrict_indep_iff, h,
restrict_indep_iff]
rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]