end — Mathlib

English

The end of a graph is defined as the sections of its component-compliment functor.

Русский

Конец графа определяется как секции функторa компонентного дополнения.

LaTeX

$$$\\mathrm{End}(G) = (\\mathrm{componentComplFunctor}\\, G).\\mathrm{sections}$$$

Lean4

/-- The end of a graph, defined as the sections of the functor `component_compl_functor` . -/
protected def «end» :=
  (componentComplFunctor G).sections

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