contract_ground

Mathlib.Combinatorics.Matroid.Minor.Contract

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

English

The ground set of the contracted matroid M / C is the original ground set with C removed: (M / C).E = M.E \\ C.

Русский

У матроида, полученного после сокращения M / C, множество оснований — это M.E без C: (M / C).E = M.E \\ C.

LaTeX

$$$ (M / C).E = M.E \\ C $$$

Lean4

@[simp]
theorem contract_ground (M : Matroid α) (C : Set α) : (M ／ C).E = M.E \ C :=
  rfl

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

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

Разделы

Аффилиация

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