isBasis_subset — Mathlib

English

If I is a basis of X and I ⊆ Y ⊆ X, then I is a basis of Y.

Русский

Если I — база X и I ⊆ Y ⊆ X, то I — база Y.

LaTeX

$$$ M.IsBasis I X \land I \subseteq Y \land Y \subseteq X \Rightarrow M.IsBasis I Y $$$

Lean4

theorem isBasis_subset (hI : M.IsBasis I X) (hIY : I ⊆ Y) (hYX : Y ⊆ X) : M.IsBasis I Y :=
  by
  rw [isBasis_iff (hYX.trans hI.subset_ground), and_iff_right hI.indep, and_iff_right hIY]
  exact fun J hJ hIJ hJY ↦ hI.eq_of_subset_indep hJ hIJ (hJY.trans hYX)

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