union_isBasis_union_of_contract_isBasis

English

If I is a basis' of X and J ⊆ I, then contracting J yields a basis' of I \ J and X \ J.

Русский

Если I является базисом' X and J ⊆ I, то сокращение J даёт базис' для I \ J и X \ J.

LaTeX

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

Lean4

theorem union_isBasis_union_of_contract_isBasis (hI : M.Indep I) (hB : (M ／ I).IsBasis J X) :
    M.IsBasis (J ∪ I) (X ∪ I) :=
  by
  simp_rw [IsBasis, hI.contract_indep_iff, contract_ground, subset_diff, maximal_subset_iff, and_imp] at hB
  refine hB.1.1.1.2.isBasis_of_maximal_subset (union_subset_union_left _ hB.1.1.2) fun K hK hKJ hKX ↦ ?_
  rw [union_subset_iff] at hKJ
  rw [hB.1.2 (t := K \ I) disjoint_sdiff_left (by simpa [diff_union_of_subset hKJ.2])
      (diff_subset_iff.2 (by rwa [union_comm])) (subset_diff.2 ⟨hKJ.1, hB.1.1.1.1⟩),
    diff_union_of_subset hKJ.2]

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