fintype

Mathlib.Combinatorics.SimpleGraph.Dart

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Dart.fintype

← MathLib Explorer

English

If V is finite and G.Adj is decidable, then G.Dart is finite.

Русский

Если V конечен и G.Adj разрешимо, то G.Dart конечно.

LaTeX

$$$ Fintype G.Dart $$$

Lean4

instance fintype [Fintype V] [DecidableRel G.Adj] : Fintype G.Dart :=
  Fintype.ofEquiv (Σ v, G.neighborSet v)
    { toFun := fun s => ⟨(s.fst, s.snd), s.snd.property⟩
      invFun := fun d => ⟨d.fst, d.snd, d.adj⟩ }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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