overFinIso

Mathlib.Combinatorics.SimpleGraph.Maps

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

← MathLib Explorer

English

There is an isomorphism between a graph G on V and its overFin n when |V| = n.

Русский

Существует изоморфизм графа G на V и графа G.overFin n при |V| = n.

LaTeX

$$$$G \\cong_g G.overFin\\; hc$$$$

Lean4

/-- The isomorphism between `G` and `G.overFin hc`. -/
noncomputable def overFinIso (hc : Fintype.card V = n) : G ≃g G.overFin hc := by use Fintype.equivFinOfCardEq hc;
  simp [overFin]

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

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

Разделы

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

Аффилиация

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