ofBoxProdRight

Mathlib.Combinatorics.SimpleGraph.Prod

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

← MathLib Explorer

English

If (G □ H) is connected, then H is connected.

Русский

Если (G □ H) связан, то H связан.

LaTeX

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

Lean4

protected theorem ofBoxProdRight (h : (G □ H).Connected) : H.Connected :=
  by
  haveI := (nonempty_prod.1 h.nonempty).1
  haveI := (nonempty_prod.1 h.nonempty).2
  exact ⟨h.preconnected.ofBoxProdRight⟩

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

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

Разделы

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

Аффилиация

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