of_contract — Mathlib

English

If h : M.IsBasis' I X and hJC : M.IsBasis' J C and h_ind : M.Indep (I \\ C ∪ J), then (M ／ C).IsBasis' (I \\ C) (X \\ C).

Русский

Если I X образуют IsBasis' и J C образуют IsBasis', и I \\ C ∪ J независим, то в сокращенном матирoиде IsBasis' сохраняется.

LaTeX

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

Lean4

theorem of_contract (hI : (M ／ C).Indep I) : M.Indep I :=
  ((M.exists_isBasis' C).choose_spec.contract_indep_iff.1 hI).1.subset subset_union_left

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