contract_dep_iff

Mathlib.Combinatorics.Matroid.Minor.Contract

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

← MathLib Explorer

English

Same as previous: If J ⊆ J and I ⊆ J then (M ／ I).Indep (J \ I).

Русский

Аналогично ранее: если I ⊆ J, то (M ／ I).Indep (J \ I).

LaTeX

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

Lean4

theorem contract_dep_iff (hI : M.Indep I) : (M ／ I).Dep J ↔ Disjoint J I ∧ M.Dep (J ∪ I) :=
  by
  rw [dep_iff, hI.contract_indep_iff, dep_iff, contract_ground, subset_diff, disjoint_comm, union_subset_iff,
    and_iff_left hI.subset_ground]
  tauto

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

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

Разделы

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

Аффилиация

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