isBase_iff_of_spanning — Mathlib

English

If M and M′ have the same ground set E and agree on which subsets S of E are spanning, then M = M′.

Русский

Если множества M и M′ имеют одну и ту же множество основания E и согласованы по тому, какие подмножества S ⊆ E образуют покрытие, то M = M′.

LaTeX

$$$$ \forall S \subseteq M.E, (M.Spanning S \iff M'.Spanning S) \Rightarrow M = M'. $$$$

Lean4

theorem isBase_iff_of_spanning {N : Matroid α} (hR : N ≤r M) (hN : M.Spanning N.E) :
    N.IsBase B ↔ (M.IsBase B ∧ B ⊆ N.E) :=
  by
  obtain ⟨R, hR : R ⊆ M.E, rfl⟩ := hR
  rw [Spanning.isBase_restrict_iff (show M.Spanning R from hN), restrict_ground_eq]

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