contract_isBasis_of_indep — Mathlib

English

If h is a basis I X in M and I ∪ J is independent, then (M ／ J).IsBasis' (I \\ J) (X \\ J).

Русский

Если базис I X существует в M и I ∪ J независим, то после сокращения по J матроид имеет IsBasis' (I \\ J) (X \\ J).

LaTeX

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

Lean4

theorem contract_isBasis_of_indep (h : M.IsBasis I X) (h_ind : M.Indep (I ∪ J)) : (M ／ J).IsBasis (I \ J) (X \ J) :=
  h.contract_isBasis (h_ind.subset subset_union_right).isBasis_self (by simpa)

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