exists_isBasis_subset_union_isBasis

English

If I is independent in M and I ⊆ X and J is a basis in X, there exists I' with I ⊆ I' ⊆ I ∪ J that is a basis in X.

Русский

Если I независим в M и I ⊆ X, а J — база в X, существует I' с I ⊆ I' ⊆ I ∪ J, такая что I' является базой в X.

LaTeX

$$∃ I' , M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J$$

Lean4

theorem exists_isBasis_subset_union_isBasis (hI : M.Indep I) (hIX : I ⊆ X) (hJ : M.IsBasis J X) :
    ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J :=
  by
  obtain ⟨I', hI', hII', hI'IJ⟩ :=
    (hI.indep_restrict_of_subset hIX).exists_isBase_subset_union_isBase (IsBasis.isBase_restrict hJ)
  rw [isBase_restrict_iff] at hI'
  exact ⟨I', hI', hII', hI'IJ⟩

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