PartsCardLe — Mathlib

English

A partition P has at most n parts if there exists a finite witness h for P.parts and its finite cardinal is ≤ n.

Русский

Разбиение P содержит не более n частей, если существует конечный свидетель h для P.parts с_card ≤ n.

LaTeX

$${P : G.Partition} \$P.PartsCardLe\\ n\$$$

Lean4

/-- Whether a partition `P` has at most `n` parts. A graph with a partition
satisfying this predicate called `n`-partite. (See `SimpleGraph.Partitionable`.) -/
def PartsCardLe {G : SimpleGraph V} (P : G.Partition) (n : ℕ) : Prop :=
  ∃ h : P.parts.Finite, h.toFinset.card ≤ n

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