diff_indep_contract_of_subset

Mathlib.Combinatorics.Matroid.Minor.Contract

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.diff_indep_contract_of_subset

← MathLib Explorer

English

If J is independent in M and I ⊆ J, then (M / I).Indep(J \ I).

Русский

Если J независимо в M и I ⊆ J, то (M / I).Indep(J \ I).

LaTeX

$$$ (M / I).Indep(J \ I) $$$

Lean4

theorem diff_indep_contract_of_subset (hJ : M.Indep J) (hIJ : I ⊆ J) : (M ／ I).Indep (J \ I) := by
  rwa [← (hJ.subset hIJ).union_indep_iff_contract_indep, union_eq_self_of_subset_left hIJ]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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