contract_isBasis'_diff_of_subset — Mathlib

English

If I is a basis I X and J ⊆ I, then contracting J yields a basis for I \ J and X \ J.

Русский

Если I является базисом I X и J ⊆ I, то сокращение J образует базис для I \ J и X \ J.

LaTeX

$$$ (M ／ J).IsBasis (I \ J) (X \ J) $$$

Lean4

theorem contract_isBasis'_diff_of_subset (hIX : M.IsBasis' I X) (hJI : J ⊆ I) : (M ／ J).IsBasis' (I \ J) X := by
  simpa [isBasis'_iff_isBasis_inter_ground, inter_diff_assoc, ← diff_inter_distrib_right] using
    (hIX.contract_isBasis'_diff_diff_of_subset hJI).isBasis_inter_ground

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