Partitionable — Mathlib

English

A graph G is n-partite if there exists a partition P of G with at most n parts.

Русский

Граф G является n-разбиением (n-разделимым) тогда и только тогда, когда существует разбиение P графа на не более n частей.

LaTeX

$$def Partitionable (n : ℕ) : Prop := ∃ P : G.Partition, P.PartsCardLe n$$

Lean4

/-- Whether a graph is `n`-partite, which is whether its vertex set
can be partitioned in at most `n` independent sets. -/
def Partitionable (n : ℕ) : Prop :=
  ∃ P : G.Partition, P.PartsCardLe n

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