fintypeEdgeSet — Mathlib

English

Let G be a simple graph on V. If Sym2 V is finite and G.Adj is decidable, then the edge set G.edgeSet is finite.

Русский

Пусть G — простой граф на V. Если множество пар вершин Sym2 V конечно и отношение смежности G.Adj разрешимо, то множество рёбер G.edgeSet конечно.

LaTeX

$$$\\operatorname{Fintype}(G\\.\\mathrm{edgeSet})$$$

Lean4

instance fintypeEdgeSet [Fintype (Sym2 V)] [DecidableRel G.Adj] : Fintype G.edgeSet :=
  Subtype.fintype _

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