preconnected_iff — Mathlib

English

For any subgraph H of G, the preconnected property on H is equivalent to the preconnected property on the underlying graph H.coe.

Русский

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

LaTeX

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

Lean4

protected theorem preconnected_iff {H : G.Subgraph} : H.Preconnected ↔ H.coe.Preconnected :=
  ⟨fun ⟨h⟩ => h, .mk⟩

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