connected_iff'

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.connected_iff'

English

For any subgraph H of G, H.Connected is equivalent to H.coe.Connected.

Русский

Для любого подграфа H графа G связность H эквивалентна связности базового графа H.

LaTeX

$$$\forall H : G{\text Subgraph},\ H.Connected \iff H.coe.Connected$$$

Lean4

protected theorem connected_iff' {H : G.Subgraph} : H.Connected ↔ H.coe.Connected :=
  ⟨fun ⟨h⟩ => h, .mk⟩

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

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

Разделы

Аффилиация

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