contract_isBasis — Mathlib

English

If h is a basis I X in M and hJC is a basis' J C with h_ind: I ∖ C ∪ J independent, then (M / C) isBasis (I ∖ C) (X ∖ C).

Русский

Если базис I X существует в M и J C образуют базис' так, что I ∖ C ∪ J независимы, то в сокращенном по C матроиде M / C образует базис (I ∖ C) внутри (X ∖ C).

LaTeX

$$$(M / C).IsBasis (I \\ C) (X \\ C)$$$

Lean4

theorem contract_isBasis (h : M.IsBasis I X) (hJC : M.IsBasis J C) (h_ind : M.Indep (I \ C ∪ J)) :
    (M ／ C).IsBasis (I \ C) (X \ C) :=
  h.contract_isBasis_of_isBasis' hJC.isBasis' h_ind

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