contract_indep_iff

Mathlib.Combinatorics.Matroid.Minor.Contract

URI: https://scilib.ai/kg/mathlib#Matroid.IsBasis.contract_indep_iff

English

If I is a basis' for X, then contract_isBasis'_diff_diff_of_subset gives a relation between (M ／ J) IsBasis' (I \ J) and (X \ J).

Русский

Если I базис' X, то контрактное отношение даёт базис' (I \ J) по (X \ J).

LaTeX

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

Lean4

theorem contract_indep_iff (hI : M.IsBasis I X) : (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J :=
  hI.isBasis'.contract_indep_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru