isBase_restrict_iff — Mathlib

English

If I X is a basis and X is spanning, then I is a base.

Русский

Если I является базисом для X и X является образующим, то I — база.

LaTeX

$$$$ (M.IsBasis I X) \rightarrow (M.Spanning X) \rightarrow M.IsBase I. $$$$

Lean4

theorem isBase_restrict_iff (hS : M.Spanning S) : (M ↾ S).IsBase B ↔ M.IsBase B ∧ B ⊆ S :=
  by
  rw [isBase_restrict_iff', isBasis'_iff_isBasis]
  refine ⟨fun h ↦ ⟨?_, h.subset⟩, fun h ↦ h.1.indep.isBasis_of_subset_of_subset_closure h.2 ?_⟩
  · exact h.indep.isBase_of_spanning <| by rwa [h.spanning_iff_spanning]
  rw [h.1.closure_eq]
  exact hS.subset_ground

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