contract_eq_delete_of_subset_loops

Mathlib.Combinatorics.Matroid.Minor.Contract

URI: https://scilib.ai/kg/mathlib#Matroid.contract_eq_delete_of_subset_loops

English

If X is a subset of the loops of M, contracting by X is the same as deleting X from M.

Русский

Если X ⊆ петли матроида M, сокращение по X эквивалентно удалению X из M.

LaTeX

$$$X \\subseteq M.loops \\Rightarrow M / X = M \\setminus X$$$

Lean4

theorem contract_eq_delete_of_subset_loops (hX : X ⊆ M.loops) : M ／ X = M ＼ X := by
  simp [(empty_isBasis_iff.2 hX).contract_eq_contract_delete]

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

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

Разделы

Аффилиация

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