connected_iff — Mathlib

English

For any subgraph H of G, H.Connected holds iff H.Preconnected holds and H.verts is nonempty.

Русский

Для любого подграфа H графа G связность H эквивалентна тому, что H предварительно соединён и множество вершин не пусто.

LaTeX

$$$\forall H : G{\text Subgraph},\ H.Connected \iff (H.Preconnected \land H.verts.Nonempty)$$$

Lean4

protected theorem connected_iff {H : G.Subgraph} : H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty := by
  rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]

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