isBase_of_minimal — Mathlib

English

If X is spanning and every Y spanning subset of X satisfies X = Y, then X is a base.

Русский

Если X образует, и для любых Y с M.Spanning Y ⟹ Y = X, то X является базой.

LaTeX

$$$$ M.Spanning X \rightarrow (\forall Y, M.Spanning Y \rightarrow Y \subseteq X \rightarrow X = Y) \rightarrow M.IsBase X. $$$$

Lean4

theorem isBase_of_minimal (hX : M.Spanning X) (h : ∀ ⦃Y⦄, M.Spanning Y → Y ⊆ X → X = Y) : M.IsBase X := by
  rwa [isBase_iff_minimal_spanning, minimal_subset_iff, and_iff_right hX]

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