instFintypeElemSym2EdgeSetFromEdgeSetOfDecidableEq

English

There is a finite type instance for the elements of the edge set of fromEdgeSet s, provided DecidableEq V and Fintype s.Elem.

Русский

Существует конечный тип элементов множества рёбер графа fromEdgeSet s при DecidableEq V и Fintype s.Elem.

LaTeX

$$$\\text{Fintype }(\\mathrm{fromEdgeSet}(s).\\mathrm{edgeSet}.\\mathrm{Elem})$$$

Lean4

instance [DecidableEq V] [Fintype s] : Fintype (fromEdgeSet s).edgeSet :=
  by
  rw [edgeSet_fromEdgeSet s]
  infer_instance

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