ground_indep_iff_isBase — Mathlib

English

Independence of the ground set is equivalent to being a base of the ground set.

Русский

Независимость множества оснований E эквивалентна тому, что E является базой самого множества E.

LaTeX

$$M.Indep(M.E) \\iff M.IsBase(M.E)$$

Lean4

theorem ground_indep_iff_isBase : M.Indep M.E ↔ M.IsBase M.E :=
  ⟨fun h ↦ h.isBase_of_maximal (fun _ hJ hEJ ↦ hEJ.antisymm hJ.subset_ground), IsBase.indep⟩

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