IsMatchingFree

Mathlib.Combinatorics.SimpleGraph.Matching

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsMatchingFree

Lean4

/-- A graph is matching free if it has no perfect matching. It does not make much sense to
consider a graph being free of just matchings, because any non-trivial graph has those.
-/
def IsMatchingFree (G : SimpleGraph V) :=
  ∀ M : Subgraph G, ¬M.IsPerfectMatching

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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