card_edgeFinset_eq

Mathlib.Combinatorics.SimpleGraph.Finite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Iso.card_edgeFinset_eq

← MathLib Explorer

English

If two graphs are isomorphic, they have the same number of edges.

Русский

Если два графа изоморфны, то у них одинаковое число рёбер.

LaTeX

$$$ #G.edgeFinset = #G'.edgeFinset $$$

Lean4

theorem card_edgeFinset_eq (f : G ≃g G') [Fintype G.edgeSet] [Fintype G'.edgeSet] : #G.edgeFinset = #G'.edgeFinset :=
  by
  apply Finset.card_eq_of_equiv
  simp only [Set.mem_toFinset]
  exact f.mapEdgeSet

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

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

Разделы

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

Аффилиация

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