restrict_eq_restrict_iff — Mathlib

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]

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