fintypeEdgeSetBot

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

The bottom graph on V has a finite edge set.

Русский

Нижний граф на V имеет конечное множество рёбер.

LaTeX

$$$\\operatorname{Fintype}(\\,\\bot : \\text{SimpleGraph } V\\,).\\mathrm{edgeSet}$$$

Lean4

instance fintypeEdgeSetBot : Fintype (⊥ : SimpleGraph V).edgeSet :=
  by
  rw [edgeSet_bot]
  infer_instance

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

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

Разделы

Аффилиация

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