isBase_iff_minimal_spanning — Mathlib

English

A base is equivalent to minimal spanning subset.

Русский

База эквивалентна минимальному образующему подмножеству.

LaTeX

$$$$ M.IsBase B \iff Minimal M.Spanning B. $$$$

Lean4

theorem isBase_iff_minimal_spanning : M.IsBase B ↔ Minimal M.Spanning B :=
  by
  rw [minimal_subset_iff]
  refine ⟨fun h ↦ ⟨h.spanning, fun _ ↦ h.eq_of_superset_spanning⟩, fun ⟨h, h'⟩ ↦ ?_⟩
  obtain ⟨B', hB', hBB'⟩ := h.exists_isBase_subset
  rwa [h' hB'.spanning hBB']

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