not_indep

Mathlib.Combinatorics.Matroid.Circuit

URI: https://scilib.ai/kg/mathlib#Matroid.IsCircuit.not_indep

English

If C is a circuit, then C is not independent.

Русский

Если C является циклом, то C не независим.

LaTeX

$$$ \\forall hC, \\ M.IsCircuit C \\Rightarrow \\neg M.Indep C $$$

Lean4

theorem not_indep (hC : M.IsCircuit C) : ¬M.Indep C :=
  hC.dep.not_indep

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

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

Разделы

Аффилиация

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