Represents — Mathlib

English

A set s of vertices represents a set C of connected components if the map G.connectedComponentMk induces a bijection between s and C.

Русский

Набор вершин s представляет набор компонент связности C, если отображение G.connectedComponentMk задаёт биекцию между s и C.

LaTeX

$$$ \\text{Represents } (s) (C) \\iff \\ Set.BijOn G.connectedComponentMk s C $$$

Lean4

/-- A set of vertices represents a set of components if it contains exactly one vertex from
each component. -/
def Represents (s : Set V) (C : Set G.ConnectedComponent) : Prop :=
  Set.BijOn G.connectedComponentMk s C

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