isBase_iff_indep_closure_eq — Mathlib

English

A set B is a base if and only if B is independent and cl(B) = E.

Русский

Множество B является базисом тогда и только тогда, когда оно независимо и cl(B) = E.

LaTeX

$$$\mathrm{IsBase}(B) \iff \mathrm{Indep}(B) \land \operatorname{cl}(B) = E$$$

Lean4

theorem isBase_iff_indep_closure_eq : M.IsBase B ↔ M.Indep B ∧ M.closure B = M.E :=
  by
  rw [← isBasis_ground_iff, isBasis_iff_indep_subset_closure, and_congr_right_iff]
  exact fun hI ↦
    ⟨fun h ↦ (M.closure_subset_ground _).antisymm h.2, fun h ↦ ⟨(M.subset_closure B).trans_eq h, h.symm.subset⟩⟩

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