contract_isBasis_diff_diff_of_subset

English

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

Русский

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

LaTeX

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

Lean4

theorem contract_isBasis_diff_diff_of_subset (hIX : M.IsBasis I X) (hJI : J ⊆ I) : (M ／ J).IsBasis (I \ J) (X \ J) :=
  by
  have h := (hIX.isBasis'.contract_isBasis'_diff_of_subset hJI).isBasis_inter_ground
  rwa [contract_ground, ← inter_diff_assoc, inter_eq_self_of_subset_left hIX.subset_ground] at h

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