Coindep — Mathlib

English

Coindep is defined as independence in the dual of the matroid; a set I is coindependent in M iff I is independent in M✶.

Русский

Коиндеп определяется как независимость в двойственном матроиде; множество I коиндепендентно в M тогда и только тогда, когда I независимо в M✶.

LaTeX

$$$ \operatorname{Coindep}(M,I) \iff M^{\ast}.Indep(I)$$$

Lean4

/-- A coindependent set of `M` is an independent set of the dual of `M✶`. we give it a separate
  definition to enable dot notation. Which spelling is better depends on context. -/
abbrev Coindep (M : Matroid α) (I : Set α) : Prop :=
  M✶.Indep I

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