instFintypeDigraphOfDecidableEq — Mathlib

English

If V is a finite type, then the class of all directed graphs on V is finite; equivalently, the collection of digraphs on V carries a finite type structure.

Русский

Если множество V конечно и задано корректо равенство, то множество всех ориентированных графов на V конечно.

LaTeX

$$$\\text{If }|V|<\\infty,\\; \\mathrm{Digraph}(V)\\text{ is finite.}$$$

Lean4

instance {V : Type*} [DecidableEq V] [Fintype V] : Fintype (Digraph V) :=
  Fintype.ofBijective Digraph.mk' <| by
    classical
    refine ⟨Embedding.injective _, ?_⟩
    intro G
    use fun v w ↦ G.Adj v w
    ext v w
    simp

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