English
Same as ext_spanning: two matroids with same ground and same spanning predicate are equal.
Русский
То же самое, что и выше: два матроидa с одинаковым основанием и одинаковыми предикатами порождения равны.
LaTeX
$$$$ \text{(Same as above)} $$$$
Lean4
theorem ext_spanning {M M' : Matroid α} (h : M.E = M'.E) (hsp : ∀ S, S ⊆ M.E → (M.Spanning S ↔ M'.Spanning S)) :
M = M' :=
by
have hsp' : M.Spanning = M'.Spanning := by
ext S
refine
(em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE])
(fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground) (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
rw [← dual_inj, ext_iff_indep, dual_ground, dual_ground, and_iff_right h]
intro I hIE
rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
