oddComponents — Mathlib

English

The odd components are defined as the connected components whose vertex-set has odd cardinality (excluding infinite components).

Русский

Нечетные компоненты — это те связные компоненты графа, у которых множество вершин имеет нечетную мощность (исключая бесконечные компоненты).

LaTeX

$$$\text{oddComponents} := \{ c : G.ConnectedComponent \mid \text{Odd } c.supp.ncard\}$$$

Lean4

/-- The odd components are the connected components of odd cardinality. This definition excludes
infinite components. -/
abbrev oddComponents : Set G.ConnectedComponent :=
  {c : G.ConnectedComponent | Odd c.supp.ncard}

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