exists_isBase_subset_spanning — Mathlib

English

If I is independent, S is spanning, and I ⊆ S, then there exists B with I ⊆ B ⊆ S and B a base.

Русский

Если I независимо и S образует, и I ⊆ S, то существует база B с I ⊆ B ⊆ S.

LaTeX

$$$$ M.Indep I \land M.Spanning S \land I \subseteq S \Rightarrow \exists B, M.IsBase B \land I \subseteq B \land B \subseteq S. $$$$

Lean4

theorem exists_isBase_subset_spanning (hI : M.Indep I) (hS : M.Spanning S) (hIS : I ⊆ S) :
    ∃ B, M.IsBase B ∧ I ⊆ B ∧ B ⊆ S :=
  by
  obtain ⟨B, hB⟩ := hI.subset_isBasis_of_subset hIS
  exact ⟨B, hB.1.isBase_of_spanning hS, hB.2, hB.1.subset⟩

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