instFintypeElemSym2EdgeSetEdge

Mathlib.Combinatorics.SimpleGraph.Operations

URI: https://scilib.ai/kg/mathlib#SimpleGraph.instFintypeElemSym2EdgeSetEdge

English

The edge set of the graph consisting of a single edge between s and t is finite.

Русский

Множество ребер графа, состоящего из одного ребра между s и t, конечно.

LaTeX

$$$Fintype\$(edge\\ s\\ t).edgeSet\$$$$

Lean4

instance : Fintype (edge s t).edgeSet := by rw [edge]; infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru