isBase_iff_maximal_indep — Mathlib

English

A base B is equivalent to B being a maximal independent set.

Русский

База B эквивалентна тому, что B — максимальное независимое множество.

LaTeX

$$$ M.IsBase B \iff Maximal M.Indep B $$$

Lean4

theorem isBase_iff_maximal_indep : M.IsBase B ↔ Maximal M.Indep B :=
  by
  rw [maximal_subset_iff]
  refine ⟨fun h ↦ ⟨h.indep, fun _ ↦ h.eq_of_subset_indep⟩, fun ⟨h, h'⟩ ↦ ?_⟩
  obtain ⟨B', hB', hBB'⟩ := h.exists_isBase_superset
  rwa [h' hB'.indep hBB']

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