isBase_of_maximal — Mathlib

English

If I is independent and maximal among supersets, then I is a base.

Русский

Если I независимо и максимально среди надмножеств, тогда I является базой.

LaTeX

$$$ M.Indep I \rightarrow (\forall J, M.Indep J \rightarrow I \subseteq J \rightarrow I = J) \rightarrow M.IsBase I $$$

Lean4

theorem isBase_of_maximal (hI : M.Indep I) (h : ∀ ⦃J⦄, M.Indep J → I ⊆ J → I = J) : M.IsBase I := by
  rwa [isBase_iff_maximal_indep, maximal_subset_iff, and_iff_right hI]

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