subset_isBasis'_of_subset — Mathlib

English

If I is independent and I ⊆ X, there exists J with J a Basis' of X containing I.

Русский

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

LaTeX

$$$ M.Indep I \land I \subseteq X \Rightarrow \exists J, M.IsBasis' J X \land I \subseteq J $$$

Lean4

theorem subset_isBasis'_of_subset (hI : M.Indep I) (hIX : I ⊆ X) : ∃ J, M.IsBasis' J X ∧ I ⊆ J :=
  by
  simp_rw [isBasis'_iff_isBasis_inter_ground]
  exact hI.subset_isBasis_of_subset (subset_inter hIX hI.subset_ground)

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