spanning_iff_exists_isBase_subset'

English

Let M.Spanning S hold. Then there exists B with M.IsBase B and B ⊆ S, together with S ⊆ M.E.

Русский

Пусть M_spanning S. Тогда существует B, такая что M.IsBase B и B ⊆ S, причём S ⊆ E.

LaTeX

$$$$ M.Spanning S \iff (\exists B\, (M.IsBase B ∧ B \subseteq S)) \\land S \subseteq M.E. $$$$

Lean4

/-- A version of `Matroid.spanning_iff_exists_isBase_subset` in which the `S ⊆ M.E` condition
appears in the RHS of the equivalence rather than as a hypothesis. -/
theorem spanning_iff_exists_isBase_subset' : M.Spanning S ↔ (∃ B, M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E :=
  by
  refine ⟨fun h ↦ ⟨?_, h.subset_ground⟩, fun ⟨⟨B, hB, hBS⟩, hSE⟩ ↦ hB.spanning.superset hBS⟩
  obtain ⟨B, hB⟩ := M.exists_isBasis S
  have hB' := hB.isBasis_closure_right
  rw [h.closure_eq, isBasis_ground_iff] at hB'
  exact ⟨B, hB', hB.subset⟩

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