contract_isBasis_union_union — Mathlib

English

If I is independent in M and (M / I) has a basis J with X then J ∪ I is a basis in M.

Русский

Если I независим в M и (M / I) имеет базис J с X, то J ∪ I является базисом в M.

LaTeX

$$$ M.IsBasis I \;\text{and}\; (M / I).IsBasis J X \Rightarrow M.IsBasis(J \cup I, X \cup I) $$$

Lean4

theorem contract_isBasis_union_union (h : M.IsBasis (J ∪ I) (X ∪ I)) (hJI : Disjoint J I) (hXI : Disjoint X I) :
    (M ／ I).IsBasis J X :=
  by
  refine (isBasis'_iff_isBasis ?_).1 <| h.isBasis'.contract_isBasis_union_union hJI hXI
  rw [contract_ground, subset_diff, and_iff_left hXI]
  exact subset_union_left.trans h.subset_ground

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