boxProd

Mathlib.Combinatorics.SimpleGraph.Prod

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Connected.boxProd

← MathLib Explorer

English

If G and H are connected graphs, then their box product G □ H is connected.

Русский

Если графы G и H связны, то их box-продукт G □ H также связан.

LaTeX

$$G.Connected ∧ H.Connected → (G □ H).Connected$$

Lean4

protected theorem boxProd (hG : G.Connected) (hH : H.Connected) : (G □ H).Connected :=
  by
  haveI := hG.nonempty
  haveI := hH.nonempty
  exact ⟨hG.preconnected.boxProd hH.preconnected⟩

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

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

Разделы

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

Аффилиация

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