contract_diff_isBasis_diff — Mathlib

English

If I is a basis X and J ⊆ I, then (M ／ J).IsBasis (I \ J) (X \ J).

Русский

Если I является базисом X и J ⊆ I, то (M ／ J).IsBasis(I \ J) (X \ J).

LaTeX

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

Lean4

theorem contract_diff_isBasis_diff (hIX : M.IsBasis I X) (hJY : M.IsBasis J Y) (hIJ : I ⊆ J) :
    (M ／ I).IsBasis (J \ I) (Y \ X) :=
  by
  refine (hJY.contract_isBasis_diff_diff_of_subset hIJ).isBasis_subset ?_ ?_
  · rw [subset_diff, and_iff_right (diff_subset.trans hJY.subset),
      hIX.eq_of_subset_indep (hJY.indep.inter_right X) (subset_inter hIJ hIX.subset) inter_subset_right,
      diff_self_inter]
    exact disjoint_sdiff_left
  refine diff_subset_diff_right hIX.subset

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