contract_isBasis' — Mathlib

English

If h is a basis' I X in M and hJC is a basis' J C in M, and h_ind is an independence condition on I \\ C ∪ J, then in the contracted matroid M / C the pair (I \\ C, X \\ C) forms a basis'.

Русский

Если h — это базис' I X в M, и hJC — базис' J C в M, и выполняется условие независимости I \\ C ∪ J, то в сокращенном матроидe 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) :=
  by
  rw [isBasis'_iff_isBasis_inter_ground, contract_ground, ← diff_inter_distrib_right]
  exact h.isBasis_inter_ground.contract_isBasis_of_isBasis' hJC h_ind

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