coindep_def

Mathlib.Combinatorics.Matroid.Dual

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

English

A set X is coindependent in M if and only if X is independent in the dual matroid of M.

Русский

Множество X коиндепендентно в M тогда и только тогда, когда X независимо в двойственном матроидe M.

LaTeX

$$$ M.Coindep X \iff M^{\ast}.Indep X $$$

Lean4

theorem coindep_def : M.Coindep X ↔ M✶.Indep X :=
  Iff.rfl

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

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

Разделы

Аффилиация

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