contract_isBasis_of_disjoint — Mathlib

English

If h is a basis I X and hJC is a basis J C with C disjoint from X, and I ∪ J is independent, then contracting by C leaves I X as a basis.

Русский

Если I X образуют базис, J C образуют базис и C не пересекает X, а I ∪ J независимы, то сокращение по C сохраняет базис I X.

LaTeX

$$$(M IsBasis I X) → (Disjoint C X) → (M ／ C).IsBasis I X$$$

Lean4

theorem contract_isBasis_of_disjoint (h : M.IsBasis I X) (hJC : M.IsBasis J C) (hdj : Disjoint C X)
    (h_ind : M.Indep (I ∪ J)) : (M ／ C).IsBasis I X :=
  by
  have h' := h.contract_isBasis hJC
  rwa [(hdj.mono_right h.subset).sdiff_eq_right, hdj.sdiff_eq_right, imp_iff_right h_ind] at h'

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