contract_isBasis'_diff_diff_of_subset

English

If I is a basis' for X and J ⊆ I, then (M ／ J).IsBasis' (I \ J) X.

Русский

Если I является базисом' для X и J ⊆ I, то (M ／ J).IsBasis' (I \ J) X.

LaTeX

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

Lean4

theorem contract_isBasis'_diff_diff_of_subset (hIX : M.IsBasis' I X) (hJI : J ⊆ I) : (M ／ J).IsBasis' (I \ J) (X \ J) :=
  by
  suffices ∀ ⦃K⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I by
    simpa +contextual [IsBasis', (hIX.indep.subset hJI).contract_indep_iff, subset_diff, maximal_subset_iff,
      disjoint_sdiff_left, union_eq_self_of_subset_right hJI, hIX.indep, diff_subset.trans hIX.subset, diff_subset_iff,
      subset_antisymm_iff, union_comm J]
  exact fun K hJK hKJi hKX hIJK ↦ by simp [hIX.eq_of_subset_indep hKJi hIJK (union_subset hKX (hJI.trans hIX.subset))]

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