Dep

Mathlib.Combinatorics.Matroid.Basic

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

English

A subset D of M.E is Dependent if it is not Independent.

Русский

Подмножество D из M.E является зависимым тогда и только тогда, когда оно не независимо.

LaTeX

$$Matroid.Dep(M, D) = (¬M.Indep D ∧ D ⊆ M.E)$$

Lean4

/-- A subset of `M.E` is `Dep`endent if it is not `Indep`endent . -/
def Dep (M : Matroid α) (D : Set α) : Prop :=
  ¬M.Indep D ∧ D ⊆ M.E

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

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

Разделы

Аффилиация

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