preconnected

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

English

If H is a connected subgraph, then H is preconnected.

Русский

Если подграф H связный, то он является предсоединённым.

LaTeX

$$$\forall H : G{\text Subgraph},\ H.Connected \Rightarrow H.Preconnected$$$

Lean4

protected theorem preconnected {H : G.Subgraph} (h : H.Connected) : H.Preconnected := by rw [H.connected_iff] at h;
  exact h.1

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

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

Разделы

Аффилиация

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