compl_isBase_dual

Mathlib.Combinatorics.Matroid.Dual

URI: https://scilib.ai/kg/mathlib#Matroid.IsBase.compl_isBase_dual

English

If h is a base of M, then M✶.IsBase (M.E \ B).

Русский

Если B является базисом M, тогда дуал на дополнении M.E \ B является базисом дуала.

LaTeX

$$∀ {α} {M : Matroid α} {B : Set α}, M.IsBase B → M✶.IsBase (M.E \ B)$$

Lean4

theorem compl_isBase_dual (h : M.IsBase B) : M✶.IsBase (M.E \ B) := by
  rwa [dual_isBase_iff, diff_diff_cancel_left h.subset_ground]

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

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

Разделы

Аффилиация

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